SMV(1) 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 "are interpreted as Syn- chonous 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 contains one record for each assertion checked, spec- ifying the the truth value of the assertion and if false, a counterexample showing why the assertion is false. Addi- tional command line options are read from the file.cflags, if it exists. These options apply to all properties veri- fied. 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 property 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. -absref Use proof-based abstraction when model checking. This technique is most effective when large parts of the system being verified are not relevant to the property being verified. -bmc Use bounded model checking. This technique searchs for a counterexample of bounded length, using a SAT solver. It can prodce a counterexample, but cannot prove a property true. The length bound on the counterexample is specified by the -l switch. The bounded model checking tool "bmc" and the SAT solver "sato" must be installed in your PATH. -check name Check the named assertion. If a structure is speci- fied, 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. -enum Enumerate unknown values. This prevents propatation of "unkown" values by introducing combinatinal variables. -f Compute reachable states by forward search and restrict model checking to these states. This is particularly 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. Use- ful 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. -l length Specify the maximum counterexample length (as the number of transitions) for bounded model checking (see the switch -bmc). A value of zero transitions means search for a counterexample in the initial state. -lazy Only compile module instances on demand. This can speed up loading very large input files by orders of magnitude. However, the global circular check is skipped when using this option, so you must run SMV without -lazy to be certain your proof is valid. -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 transi- tion relation. -nodp Do not use disjunctive partitioning of the transi- tion 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. -persist Keep checking properties even after one is found to be false. -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 SIMULATION. -sif Use external model checker via the SIF interface (see below). -sifliveness The external solver supports liveness checking. -sifsolver solver Use solver as the external model checker. -sift Use sifting to attempt to improve the variable order. -smcsat2 Use SAT-based model checking (version 2). Like proof-based abstraction, this technique is most effective when large parts of the system being ver- ified are not relevant to the property being veri- fied. If you are suffering from BDD explosion using -absref, you may want to try this. -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 mod- ule 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 transi- tion relation 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 abstraction 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 veri- fying properties, the definiton of "name" will be taken from "layer". Signals which have no entry in the abstrac- tion file inherit their abstraction layer from their par- ent. 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 low- est, or "implementation" layer) and "free", which leaves the signal 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 defin- tion 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 proper- ties 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 efficiency 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 program. 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 recommended 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 vari- able declarations to the program, so that the variables are declared in the desired order, or by creating a vari- able 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 impor- tant number to look at is the number of BDD nodes repre- senting the transition relation. It is very important to minimize this number. Iterations are used to solve the fixed point equations which characterize the various tem- poral 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 hierar- chy (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 "conjunctive decompositions". Finally, foo.n, where n is a number denotes the the n-th encoding variable of foo, counting from 0 (assuming foo is not a boolean). This is useful to know in case you are editing an order file out- put 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 assignments 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 program 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 par- ticular behavior is guaranteed for nondeterministic choices that are determined by the trace input file. One of the available values will be chosen, but this choice is not made in any statistically 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). USING VW WITH XEMACS Smv can interact with the XEmacs text editor. To enable this feature, you must put the line (load-library "smv-hooks") in your ~/.emacs file, and the file "smv-hooks.el" must be in some directory in the list "load-library-path". Once "smv-hooks" is loaded, files ending in ".smv" will use smv-mode. This is very similar to c-mode, except that it supports the smv syntax. Further, if you run smv from inside an emacs shell buffer, emacs can display the file containing an error, and place a pointer "=>" on the line contining the def. To enable this, you must define the environment variable "VW_EMACS". Note, these features have been tested only using Xemacs version 19.16. They may or may not work with other ver- sions. COMPATIBILITY WITH CARNEGIE MELLON SMV This version of SMV is (mostly) source-compatible with Carnegie Mellon SMV. Modules written in the two languages may be mixed. In addition, SPEC declarations specifying CTL formulas 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. INTERFACING TO AN EXTERNAL MODEL CHECKER SMV can interface to an external model checker via the SIF file format. The protocol for doing this is described in the file "smvsif.txt", which is distributed with SMV. 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) 23 Jan 1996 1