What is SMV, CSML, and MCB ?
From: David Long (David.Long@tempura.logi.cs.cmu.edu)
SMV -- a symbolic model checker for CTL [latest revision 2.4.2]. It is
available as ftp://emc.cs.cmu.edu/pub/tape
A BDD-based symbolic model checking program (SMV) that can handle
asynchronous systems is available for FTP from tempura.logi.cs.cmu.edu. 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).
Papers on various related topics.
pub/bdd/futurebus.ps is a paper describing the formal verification of
the Futurebus+ cache coherence protocol. Click
here
to get a copy.
pub/tape/ISSMM.ps is a paper describing the formal verification of the
Gigamax cache cohernce protocol. Click
here
to get a copy.
pub/tape/SMC.ps is the paper "Symbolic Model Checking: 10^20 States
and Beyond". Click
here
to get a copy.
Everything is available on tempura.logi.cs.cmu.edu.