The following link demonstrates how to connect Icarus Verilog with NuSMV for equivalence checking:
http://www.confluent.org/wiki/doku.php?id=docs:using_nusmv_for_formal_verification
-Tom
Release 0.10.4 adds support for multipliers in the FNF NuSMV code
generator. In addition, the NuSMV generator transforms top-level
outputs into assertions. This makes it possible to construct
verification-benches in either Confluence or Verilog, and prove the
correctness of a design using NuSMV.
The following link demonstrates how to connect Icarus Verilog with NuSMV for equivalence checking:
The following link demonstrates how to connect Icarus Verilog with NuSMV for equivalence checking:
