SMV(1) User Commands SMV(1) NAME smv - symbolic model verifier SYNOPSIS smv -switch[val]... option=value... -Idir... -Dsym=val... file.[smv,v] DESCRIPTION Verify or simulate a program in the SMV language, or Syn- chronous Verilog language, using symbolic model checking techniques. This is intended mainly for batch use. For interactive use, see vw(1). All input files are piped through a preprocessor much like the C preprocessor. Files on the command line, or in "#include" directives, with extension ".v", are interpreted as Synchonous Verilog, and are translated to SMV by vl2smv(1). If -check switch is present (see below), checks only the properties with the given name, or descendants of the given name. Results are stored in file "file.out". This file con- tains one record for each assertion checked, specifying the the truth value of the assertion and if false, a counterex- ample showing why the assertion is false. Additional command line options are read from the file.cflags, if it exists. These options apply to all properties verified. Property- specific options are read from the file "file.options". See "Options file" below for the format of this file. If "file.cflags" does not exist, and options for a given pro- perty are not specified in "file.options", then the default options "-v 1 -f -h" are added to the command line options. The default options can be disabled on the command line with the switch "--". Options are specified on the command line in the form option=value, where "option" is the option name, and "value" is its value. Each option has an abbreviation in the form "-switch". For boolean options, this sets the value of the switch to 1. For example, "-f" is equivalent to "ForwardSearch=1". The only way to switch this option off is "ForwardSearch=0". For non-boolean options, the option value is the next word in the command line. For example, "-v 1" is equivalent to "Verbose=1". OPTIONS This is a partial list of the available options, in the "- switch" form only. Use "smv -help" for a complete list, including the "option=value" form. -- Do not use the default options. -abs filename Specifies the abstraction file. -check name Check the named assertion. If a structure is specified, all assertions contained in that structure are checked. -de Use conjunctive decompositions in model checking. -Dsymbol=value Define a symbol for the preprocessor, as in cc. -f Compute reachable states by forward search and res- trict model checking to these states. This is particu- larly useful when checking state machines and protocols where the state-space is sparse. It is not recommended for checking data paths. -foo filename Output final variable order (after model checking and sifting) to file filename. -fsift Sift just once, after all properties checked. Useful only with -foo. -Ipathname Look in directory "pathname" for include files, as in cc. -i variable-order-file Read the BDD variable order from the given file. This allows the variable order to be modified with a text editor. See "Variable order file" below for the format of this file. See alo the -o switch. -m module-name Treat the named module as the main module. -nopr Do not used partitioned transition relations. -nocp Do not use conjunctive partitioning of the transition relation. -nodp Do not use disjunctive partitioning of the transition relation. -o variable-order-file Output the variable BDD variable order to the given file and stop without checking any assertions. See also -i option. -pf number Profile any BDD's larger than the given number of nodes. -run trace-file Run a the simulation trace described in the given file. Format of this file is described below under SIMULA- TION. -sift Use sifting to attempt to improve the variable order. -stubs filename This file lists names of structures (one to a line) that are not to be used in the verification. This is chiefly used to avoid parsing a very large module in the hierarchy that is not relevant to the assertions being checked. -together Check all properties in a property group in the same model checker run. This means that the transition rela- tion and the reached state set will be computed only once for the group. -v number A non-zero value causes a transcript of the run to be printed on the standard output. Higher numbers cause more output. -Z Initialize any uninitialized state variables to zero. This is useful for large codes translated from verilog that do not initialize registers. It is also completely bogus. THE OPTIONS FILE The file "file.options" is used to set property specific options. It consists of lines of the form: name : "command line options"; (where the quotation marks are necessary). This sets the options of any property which is a descendant of "name", and not otherwise set. ABSTRACTION FILES When verifying a given property, you can use definitions of signals at a chosen level of abstraction. This defines the "environment" for verifying the given property. The abstrac- tion file consists of lines of the form name//layer where "name" is a name in the signal name hierarchy of the program and "layer" is a layer in the program. When verify- ing properties, the definiton of "name" will be taken from "layer". Signals which have no entry in the abstraction file inherit their abstraction layer from their parent. This makes it possible to set the abstraction layer for an entire module instance with a single line in the abstraction file. In addition to the layers defined in the program, "layer" may also take on the value "." (which stands for the lowest, or "implementation" layer) and "free", which leaves the sig- nal undefined (free to take any value at any time). If no layer is specified for a given signal, the highest (most abstract) available layer is used. There are three cases when the layer specified in the abstraction file may not be used by the model checker: 1) If the given signal is not defined in the given layer, the model checker will choose the next lower layer in which the signal is defined. 2) If you are verifying refinement of foo//bar, you cannot use the definition of foo in layer bar, since this would be circular reasoning. Similarly, to cannot chose a defintion at a higher layer. In this case, smv uses the next layer below bar for the given signal. 3) The given signal may not be in the dependency cone of the property. In this cae, it is not used at all. Note that the dependency cone is a function of the chosen abstraction. PROPERTY GROUPS FILE The file "file.groups" is used to define groups of proper- ties that are treated as a single property. It consists of lines of the form group-name : {property-name, property-name, ... property- name} Note that a property name can be any name in the name hierarchy. For example, if "foo" is a module instance, then including "foo" in the group will include all properties contained in instance "foo", provided they are not listed in another group under a more specific name. As an example, suppose we have an array of properties p[0] group1 : {p} group2 : {p[2]} The group1 will contain p[0], p[1] and p[3], while group2 contains p[2]. VARIABLE ORDERING Smv uses Binary Decision Diagrams (BDDs) to represent sets and relations in the model checking algorithm. A BDD is a decision tree, in which variables always appear in the same order as the tree is traversed from root to leaf. The effi- ciency of BDDs is obtained by always combining isomorphic subtrees, and by eliminating redundant decision nodes in the tree. The degree of storage efficiency obtained in this way depends stringly on the variable ordering. There are built-in heuristics for selecting the variable ordering, and these are invoked by the default option "-h". If you disable this option (in the ".cflags", or ".options" file, or by using the "--" option), the variables appear in the BDDs in the same order in which their types are declared in the pro- gram. This means that variables declared in the same module are grouped together, which is sometimes better than the heuristic order. Sifting (see the -sift options above) can be used to attempt to improve on the variable order. This takes some extra time but usually saves space. It is recom- mended to try "-sift" if the BDD sizes become very large, however this is not a default option, as it often slows down the verification process. For the intrepid, the variable ordering may be adjusted by hand. This can be done either by adding redundant variable declarations to the program, so that the variables are declared in the desired order, or by creating a variable order file (see "Variable order file" below). A good heuristic is to arrange the ordering so that variables which often appear close to each other in formulas are close together in the order, and global variables should appear first. If the "-v 1" option (default) is used, the sizes of BDD's are printed on the transcript. An important number to look at is the number of BDD nodes representing the transi- tion relation. It is very important to minimize this number. Iterations are used to solve the fixed point equa- tions which characterize the various temporal operators, and also to search for counterexamples. With each iteration, the number of BDD nodes is printed. Some of the options can improve performance. Experiment with them if the run time or memory usage starts getting out of hand. VARIABLE ORDER FILE A variable order file specifies the initial order for the BDD variables. The syntax of this file is: order:: item item ... item item:: signal-name signal-name.# { order } item1 except item2 group item A signal name can be any point in the signal name hierarchy (e.g., the name of a simple signal, or an array, or a module instance). All the descendants of the given signal name will appear in type definition order. Only the first occurrence of a signal name counts. The construct "item1 except item2" causes signals in item2 to occur after item1 in the order, even if they occur in item1. For example, if x is an array 0..3, then x except x[2] is the same as x[0] x[1] x[3] x[2]. The "group" construct is used currently only with the -de option, which uses "con- junctive decompositions". Finally, foo.n, where n is a number denotes the the n-th encoding variable of foo, count- ing from 0 (assuming foo is not a boolean). This is useful to know in case you are editing an order file output from smv. SIMULATION A simultation trace file is a sequence of assignments to program variables. Each of these assignments overrides the value of the given variables in the given state of program execution. The format of this file is a sequence of assign- ments of the form: {a1, a2, ..., ak} where each ai is of the form vari = vali or vari := vali The former case is a "suggestion" meaning that if vali is among the possible choices for vari, then vali is chosen, but otherwise the choice is unaffected. The latter case is an "override" meaning that the value of vari is set to vali and any assignment made to vari in the program is ignored. Note, the assignment may be empty: {}. If a simulation trace file is specified with the -run option (see above), the pro- gram is simulated for the given number of steps with the given suggestions and overrides, and the result is dumped to the result file (file.out). Note that no particular behavior is guaranteed for nondeterministic choices that are deter- mined by the trace input file. One of the available values will be chosen, but this choice is not made in any statisti- cally useful way, and it is not guaranteed that all possible choices will eventually be taken. Simulation output in the result file can be viewed with vw(1). COMPATIBILITY WITH CARNEGIE MELLON SMV This version of SMV is (mostly) source-compatible with Car- negie Mellon SMV. Modules written in the two languages may be mixed. In addition, SPEC declarations specifying CTL for- mulas to check may be included in any module. These specs can be named, in the following manner: :SPEC; In general, however, constructs from the current language and the original Carnegie Mellon ver- sion may not be mixed within a single module. SEE ALSO vw(1),vl2smv(1) K.L.McMillan,The SMV language Kenneth L. McMillan, Symbolic Model Checking, Kluwer, 1993. BUGS See the relase notes. AUTHOR Kenneth L. McMillan, Cadence Berkeley Labs mcmillan@cadence.com SMV (Cadence version)Last change: 23 Jan 1996 7