[ANN] InFormal 0.1.1 Released

Discussion in 'VHDL' started by Tom Hawkins, Nov 9, 2004.

  1. Tom Hawkins

    Tom Hawkins Guest

    Hello,

    I just released InFormal 0.1.1: a new open-source assertion based
    verification tool. InFormal can prove the correctness of Verilog
    designs without using simulation -- otherwise known as formal
    verification.

    With release 0.1.1, InFormal now provides initial support for
    PSL/Sugar. Currently only a small subset of PSL is supported, but
    it's PSL never the less.

    Though InFormal is in very early beta, it has already uncovered bugs
    in real designs -- in part thanks to automatic assertions. Using
    InFormal's automatic assertions, engineers can find potential design
    issues without having to explicitly define PSL properties.

    InFormal leverages the elaboration and synthesis technology of Icarus
    Verilog with the high performance symbolic model checking engine of
    NuSMV. Many thanks to the Icarus and NuSMV teams for providing their
    awesome open-source technology.

    For more information on InFormal, including source code and Linux
    binaries, visit:

    http://www.confluent.org/

    Enjoy!

    -Tom
     
    Tom Hawkins, Nov 9, 2004
    #1
    1. Advertisements

  2. Tom Hawkins a écrit:
    > Hello,
    >
    > InFormal can prove the correctness of Verilog designs without using simulation


    I'm sure VHDL users will be very happy to know this...

    --
    ____ _ __ ___
    | _ \_)/ _|/ _ \ Adresse de retour invalide: retirez le -
    | | | | | (_| |_| | Invalid return address: remove the -
    |_| |_|_|\__|\___/
     
    Nicolas Matringe, Nov 9, 2004
    #2
    1. Advertisements

  3. Tom Hawkins

    Tom Hawkins Guest

    Nicolas Matringe <> wrote in message news:<>...
    > Tom Hawkins a écrit:
    > > Hello,
    > >
    > > InFormal can prove the correctness of Verilog designs without using simulation

    >
    > I'm sure VHDL users will be very happy to know this...


    Sounds like you're volunteering! The InFormal netlist representation
    is very straight forward. Simply write some code for GHDL to generate
    an InFormal netlist; then you're all set: formal verification with
    VHDL.

    -Tom
     
    Tom Hawkins, Nov 9, 2004
    #3
    1. Advertisements

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. Tom Hawkins

    [ANN] Confluence 0.7.1 Released

    Tom Hawkins, Oct 23, 2003, in forum: VHDL
    Replies:
    0
    Views:
    668
    Tom Hawkins
    Oct 23, 2003
  2. Jussi Jumppanen

    ANN: Zeus Version 3.95 Editor Released

    Jussi Jumppanen, Aug 8, 2005, in forum: VHDL
    Replies:
    0
    Views:
    551
    Jussi Jumppanen
    Aug 8, 2005
  3. Replies:
    1
    Views:
    480
    Stefan Ram
    Sep 14, 2005
  4. Alan Mackenzie
    Replies:
    1
    Views:
    586
    Alan Mackenzie
    Apr 24, 2005
  5. Alan Mackenzie

    Emacs CC Mode's auto-newline facility: INFORMAL SURVEY

    Alan Mackenzie, Apr 8, 2005, in forum: C Programming
    Replies:
    9
    Views:
    622
    those who know me have no need of my name
    Apr 28, 2005
  6. blangela
    Replies:
    2
    Views:
    364
    Ian Collins
    Nov 25, 2006
  7. Brian Guthrie
    Replies:
    0
    Views:
    323
    Brian Guthrie
    May 8, 2007
  8. Martijn Faassen

    informal #python2.8 channel on freenode

    Martijn Faassen, Jan 6, 2014, in forum: Python
    Replies:
    1
    Views:
    133
    Emile van Sebille
    Jan 6, 2014
Loading...