1. Home
  2. Field-Programmable Gate Arrays
  3. [ANN] InFormal 0.1.1 Released

[ANN] InFormal 0.1.1 Released

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:

formatting link

Enjoy!

-Tom

Reply to
Tom Hawkins
Loading thread data ...

Tom Hawkins a écrit:

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

--
  ____  _  __  ___
|  _  \_)/ _|/ _ \   Adresse de retour invalide: retirez le -
| | | | | (_| |_| |  Invalid return address: remove the -
|_| |_|_|\__|\___/
Reply to
Nicolas Matringe

simulation

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

Reply to
Tom Hawkins

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.