RE: gEDA: InFormal 0.1.2

["Hawkins, Thomas" <thomas.d.hawkins@xxxxxxxxxxxxx>]

The "equivalence_checking" was not part of NuSMV.  I used a commerical tool to show that the FNF transformations are correct, at least for a few testcases.

NuSMV is a model checker, not an equivalence checker.  But it can do equivalence checking if your models are small enough.  Try this:

1. Create a Verilog verification harness that integrates the two models:

module golden (a, b, x, y);
input  a, b;
output x, y;
//...
endmodule

module revised (a, b, x, y);
input  a, b;
output x, y;
//...
endmodule

module ec_harness (a, b, is_equivalent);
input  a, b;
output is_equivalent;
wire   x_0, y_0, x_1, y_1;
golden  m0 (a, b, x_0, y_0);
revised m1 (a, b, x_1, y_1);
assign is_equivalent = (x_0 == x_1) && (y_0 == y_1);
endmodule

2. Use Icarus to generate an FNF netlist of the ec_harness.

3. Use InFormal to generate an NuSMV model from the FNF netlist.

4. Add a NuSMV spec to assert that is_equivalent is always true:

  SPEC AG n22_0;  -- You will have to find the cell that is associated with is_equivalent.

5. Run NuSMV:

  > NuSMV my_model.smv




-----Original Message-----
From: owner-geda-dev@xxxxxxxx [mailto:owner-geda-dev@xxxxxxxx]On Behalf
Of Steve Tell
Sent: Wednesday, January 05, 2005 4:59 PM
To: geda-dev@xxxxxxxx
Subject: Re: gEDA: InFormal 0.1.2


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