.\" Process this file with .\" groff -man -Tascii smv2vcd.1 .\" .TH SMV2VCD 1 "DECEMBER 2001" Linux "User Manuals" .SH NAME smv2vcd \- Generate a Value Change Dump (VCD) file from a SMV counterexample .SH VERSION 1.0 .SH SYNOPSIS .B smv2vcd [ .I -h .B ] [ .I smv-counterexample .B [ .I vcd-file .B [ .I gtkwave save-file .B ]]] .SH OPTIONS .IP -h Produces a brief usage message on stdout. .IP "smv counterexample" File containing single .I SMV/NuSMV counterexample. .IP "vcd-file" Value change dump will be written to this file. .IP "gtkwave save-file" File containing format description for each signal. .I GtkWave can use this file to display signals in the format specified. .P The first two files are assumed to be stdin/stdout respectively if not specified. Use - for specifying stdin/stdout for any file. The save file is generated only if all the options are specified. .SH DESCRIPTION Reads a counterexample produced by .B SMV/NuSMV and generates a corresponding .B 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 Standard 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 facility to save the list of signals currently being viewed in .I 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 values, unless a signal is less than or equal to 3 bits long, in which case it is diaplayed in binary. .I smv2vcd produces a save file if the last options is specified. It always produces comments in the VCD file containing 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. .I smv2vcd also generates an artificial signal called .I cycle_counter that keeps track of the current clock cycle. This signal should be viewed using unsigned decimal format. .SH RELATED SOFTWARE .TP .B SMV The first BDD based model checker. More info at .I http://www.cs.cmu.edu/~modelcheck. .TP .B NuSMV Reimplementation into a feature rich model checker. Available at .I http://nusmv.irst.itc.it. .TP .B GTKWave A powerful wave viewer. Available at .I http://www.cs.man.ac.uk/amulet/tools/gtkwave/index.html .SH TO DO/BUGS 1. At present input file can contain only one SMV counterexample, 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. .SH GETTING smv2vcd This software is available at .I http://www.cs.cmu.edu/~modelcheck. .SH COPYRIGHT This man page and the software is (c) Carnegie Mellon University, 2001. .SH DISCLAIMER We are not responsible for anything, particularly anything bad, that happens by the use of this software. .SH AUTHORS Tae Jung Kim Pankajkumar Chauhan .SH "SEE ALSO" .BR smv (1)