Model Checking @CMU

[Home]

[People]

[Software]

[Publications]

[Support]

[Links]

[Internal]

 

Word-level SMV

The word-level extensions of SMV are now available for download. To obtain the code, follow the link:

wsmv.tar.Z (93K)
Clicking on the reference above retrieves the files automatically.

What is Word-level SMV ?

A word is a collection of boolean variables that represent integer or floating point numbers. The original SMV does not allow the expression of properties that relate to words, only of properties relating to the individual bits of each word. Consequently, properties of arithmetic circuits are very difficult to express and verify.

Word-level model checking overcomes this difficulty by representing words internally using HDDs (Hybrid Decision diagrams). It is now not only much simpler to express arithmetic properties, but also much more efficient to verify these properties. To show the usefulness of the new method, we provide with the source code a model for an 64-bit wide SRT division circuit that has been verified using word-level SMV.

The file wsmv.tar.Z (in "tar" format) contains the sources and some examples. To break out the directory structure, after you have gotten the files, use the commands

uncompress wsmv.tar.Z
tar -xf wsmv.tar

CMU-SCS Model Checking home page

Please send any comments and suggestions to  Nishant Sinha - (nishants) at cs dot cmu dot edu.