Model Checking @CMU










A Perl script to convert SMV/NuSMV generated counterexamples to industry standard Value Change Dump (VCD) format. Waveforms described in this format can be viewed in a wide variety of open source and commercial synthesis/simulation/wave viewer programs. This is still an alpha stage software, so the feature you may want may not be there, though we don't think there is much that can be added for such a simple task. Bugs is an altogether different matter though, please report them to pchauhan [at] cs [dot] cmu [dot] edu. Please keep in mind that this tool was made purely for research purposes.

Tae Jung Kim, Pankaj Chauhan December 2001

smv2vcd-1.0.1.tar.gz,, a bugfix version, thanks to Armin Biere. Now it can read Bwolen SMV, Cadence SMV, Armin's BMC, NuSMV etc. generated counterexamples and run on older Perl versions.

smv2vcd-1.0.tar.gz, README, man page

We are also making the free wave form viewer GtkWave available on our site as a convenience. However, the latest version can be obtained from









CMU-SCS Model Checking home page

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