BMC, SMV, CSML, CV and MCB

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 useful.

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:

• Stuff for sequential verification, such as routines for relational product and frontier set simplification
• Pointer flags for output negation, input negation, and "else negation"
• 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 these"
• 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