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:

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.