SMV2VCD(1) User Manuals SMV2VCD(1) NAME smv2vcd - Generate a Value Change Dump (VCD) file from a SMV counterexample VERSION 1.0 SYNOPSIS smv2vcd [ -h ] [ smv-counterexample [ vcd-file [ gtkwave save-file ]]] OPTIONS -h Produces a brief usage message on stdout. smv counterexample File containing single SMV/NuSMV counterexample. vcd-file Value change dump will be written to this file. gtkwave save-file File containing format description for each signal. GtkWave can use this file to display signals in the format specified. The first two files are assumed to be stdin/stdout respec­ tively if not specified. Use - for specifying stdin/stdout for any file. The save file is generated only if all the options are specified. DESCRIPTION Reads a counterexample produced by SMV/NuSMV and generates a corresponding Value Change Dump (VCD) file. A value change dump (VCD) file contains information about value changes on selected variables in the design, stored by value change dump system tasks (more info in IEEE Stan­ dard Hardware Description Language Based on the Verilog Hardware Description Language 1995 - Section 15). This is a popular format accepted by various commercial and free synthesis tools. Once the VCD file is generated then it can be viewed with a wave viewer such as the GTKWave 1.3.10. Thus, it is a widely used easy graphical way to see any SMV counterexample. A wave viewer usually does not show any signals by default, although a VCD file contains information about all signals. Those signal that a user is interested should be selected by the user in the GUI of the viewer. Selecting signals each time you view a waveform can be rather cumbersome, so GTKWave and others include a facil­ ity to save the list of signals currently being viewed in save files. These save files contain information about the data type format to use for displaying each signal, name aliases, signal grouping and so on. Without the type information, all signals are displayed as hexadecimal val­ ues, unless a signal is less than or equal to 3 bits long, in which case it is diaplayed in binary. smv2vcd produces a save file if the last options is speci­ fied. It always produces comments in the VCD file con­ taining information about datatype to be used for viewing each signal. Each enumerated signal should be viewed using ASCII format and the other signals should be viewed using signed decimal format. smv2vcd also generates an artificial signal called cycle_counter that keeps track of the current clock cycle. This signal should be viewed using unsigned decimal for­ mat. RELATED SOFTWARE SMV The first BDD based model checker. More info at http://www.cs.cmu.edu/~modelcheck. NuSMV Reimplementation into a feature rich model checker. Available at http://nusmv.irst.itc.it. GTKWave A powerful wave viewer. Available at http://www.cs.man.ac.uk/amulet/tools/gtk­ wave/index.html TO DO/BUGS 1. At present input file can contain only one SMV coun­ terexample, if you include more than one counterexample in a single file, it will be treated as a long, single sequence of states. 2. There will be examples of SMV/NuSMV counterexamples breaking this script. Please report them. GETTING smv2vcd This software is available at http://www.cs.cmu.edu/~mod­ elcheck. COPYRIGHT This man page and the software is (c) Carnegie Mellon Uni­ versity, 2001. DISCLAIMER We are not responsible for anything, particularly anything bad, that happens by the use of this software. AUTHORS Tae Jung Kim Pankajkumar Chauhan SEE ALSO smv(1) Linux DECEMBER 2001 1