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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] Behalf Of Steve Tell Sent: Wednesday, January 05, 2005 4:59 PM To: [email protected] 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
