This InFormal release includes the first implementation of FNF.
http://www.confluent.org/wiki/doku.php?id=informal:main
What's new:
- Icarus Verilog FNF code generator. - InFormal FNF reader. - InFormal FNF writer. - InFormal Verilog writer. - InFormal NuSMV writer.
With the new framework, PSL and auto assertions are temporarily disabled.
With help from the InFormal Verilog writer, a few example designs have have been used to verify the FNF implementation with the following flow:
> iverilog -Wall -t fnf -o netlist_0.fnf design.v > informal -read_fnf netlist_0.fnf -write_fnf netlist_1.fnf > informal -read_fnf netlist_1.fnf -write_fnf netlist_2.fnf > informal -read_fnf netlist_2.fnf -write_verilog revised_design.v > equivalence_checking -golden design.v -revised revised_design.v > diff netlist_1.fnf netlist_2.fnf
-Tom
