Re: gEDA: InFormal 0.1.2

[Steve Tell <tell-at-NOSPAMtelltronics_dot_org>]

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