=================================================================
TITLE: Free Verification Tools for Researchers
VIS (Verification Interacting with Synthesis) is a tool that
integrates the verification, simulation and synthesis of finite-
state hardware systems. It uses a Verilog front-end and supports
model checking of temporal logic assertions, language emptiness
checking, combinational and equivalence checking, cycle-based
simulation and hierarchical synthesis. The verification engine is
BDD-based.
For more information, access: VIS
Cadence SMV (free of use for research purposes) is a system for
checking finite state systems against properties written in
temporal logic, finite state automata, embedded assertions, and
refinement specifications. Cadence SMV supports synthesizable
Verilog as a modeling language, allowing RTL design to be
verified. For the analysis of large designs, Cadence SMV
supports compositional reasoning. However, user guidance is
necessary to perform these analyses.
For more information, access: SMV
=================================================================