On Wed, 8 Dec 2004, Tom Hawkins wrote: > This InFormal release includes the first implementation of FNF. > > http://www.confluent.org/wiki/doku.php?id=informal:main
> > 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 I'm enticed by the description, but a little confused after installing informal and NuSMV - What does the line "equivalence_checking ..." above signify? Is it actually possible to do even rudimentary verilog vs. verilog formal comparison with these tools? (I don't see an equivalence_checking command, but maybe that's a simple exercise in NuSMV?) Steve
