BMC, SMV, CSML, CV and MCB
From: David Long (David.Long@tempura.logi.cs.cmu.edu)
Additions: Andrew Bardsley [new contribution from authors required?]
All the tools on this page can be found at
CS CMU's model checking page.
BMC - a bounded model checker.
SMV -- a symbolic model checker for CTL [latest revision 2.4.2].
A BDD-based symbolic model checking program (SMV) that can handle
asynchronous systems. It is
not specifically geared to asynchronous circuits, but you may find it
CSML is a high level level language for describing finite state machines.
There is a compiler which produces a finite state machine as output.
There is also a CTL model checker called MCB which accepts the state
machine file as input. MCB is an enhanced version of the EMC model checker.
A BDD library with extensions for sequential verification is available.
The libraries main features include:
CV - CV is a model checker for VHDL
- Stuff for sequential verification, such as routines for relational
product and frontier set simplification
- Pointer flags for output negation, input negation, and "else
- Unified result cache for all operations. All operations, including
things like multi-variable quantification and simultaneous
substitution, cache across calls
- Routines for node profiles (histograms of the number of nodes at
each level) and function profiles (histograms of the number of
functions obtainable by restricting variables above each
level) for analyzing BDD sizes.
- Routines for dumping BDDs to files and loading them again
- Garbage collection via either reference counting or "keep only
- Settable node limit. Operations abort and clean up their
intermediates if they cannot finish without the total number
of nodes exceeding the limit.
- Very small and fast. Should be fairly portable across 32-bit
machines running UNIX. If you're not running UNIX, you'll
have to modify the memory management routines (the package
implements a buddy scheme and calls sbrk directly).
MCB - a non-symbolic model checker for CTL