[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. Advertising

  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. Advertising

  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. Advertising

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. Replies:
    1
    Views:
    391
    Stefan Ram
    Sep 14, 2005
  2. Alan Mackenzie
    Replies:
    1
    Views:
    464
    Alan Mackenzie
    Apr 24, 2005
  3. Alan Mackenzie

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

    Alan Mackenzie, Apr 8, 2005, in forum: C Programming
    Replies:
    9
    Views:
    450
    those who know me have no need of my name
    Apr 28, 2005
  4. blangela
    Replies:
    2
    Views:
    297
    Ian Collins
    Nov 25, 2006
  5. Brian Guthrie
    Replies:
    0
    Views:
    199
    Brian Guthrie
    May 8, 2007
Loading...

Share This Page