Tuesday, February 26, 2008

Linux: Installing Cadence SMV for Model Checking


This post is for all those computer science students who have to face the pain of doing Model checking and verification course as a part of their graduation requirements. One of the most common tool kits used for this purpose is the Cadence Berkley SMV
Get the linux binary package from here

Here are the steps to install it:



1. Extract the tar file to some folder called smv. Change to that folder and copy it to /usr/local

$sudo cp -r smv /usr/local/


2. Set path variables and links

$sudo export PATH=$PATH:/usr/local/smv/bin


$sudo ln -s /usr/local/smv/lib/libsmvcore.so /usr/lib/libsmvcore.so


$sudo ln -s /usr/local/smv/lib/libsmv.so /usr/lib/libsmv.so


3. The command line smv program should start working now. Type this and test

smv


4. To get the gui version - vw running, we need to install some additional packages. Fire up synaptics and install these 2 packages.
tk8.4 8.4.15-1ubuntu1
tix

4. vw can be run now. Run this and test

vw




PS: To run it as a normal user, you can either add the path of smv bin to profile $PATH
$sudo ln -s /usr/local/smv/bin/smv /usr/bin/smv
$sudo ln -s /usr/local/smv/bin/vw /usr/bin/vw
$sudo chmod u+x smv
$sudo chmod u+x vw


4 comments:

Anonymous said...

I got this error while running
#smv echo3.smv
Same error with vw.

Running SAT solver
==================
Variables: 6 Clauses: 14
runsmvsat: error while loading shared libraries: libstdc++-libc6.1-1.so.2: cannot open shared object file: No such file or directory
smv: error running sat solver
==================

I couldn't find libstdc++ ... lib for Ubuntu 7.10 nor for debian 3.0
How to make it work?

Thanks

Unknown said...

Hello!
I am interested to know if there is some commands for running uder the Windows version of Cadence SMV,for instance there a command to run "Verify all" within command-line interface instead of running from GUI,
have any idea?
Thank you
Massoud

Unknown said...

Hello!
I am interested to know if there is some commands for running uder the Windows version of Cadence SMV,for instance there a command to run "Verify all" within command-line interface instead of running from GUI,
have any idea?
Thank you
Massoud

alexey said...

Hello,
Did you try to use smv for verifying big models (program or hardware)?
Have you achieved some results using smv except verifying models in ../SMV/doc/examples/ ?