SMV(1)                                                                  SMV(1)



[1mNAME[0m
       smv - symbolic model verifier

[1mSYNOPSIS[0m
       [1msmv    [22m-switch[4m[val][24m...     option=value[4m...[24m     -Idir[4m...[24m    -Dsym=val[4m...[0m
       file.[smv,v]

[1mDESCRIPTION[0m
       Verify or simulate a program in the SMV language, or  Synchronous  Ver-
       ilog  language,  using  symbolic  model  checking  techniques.  This is
       intended mainly for batch use. For interactive  use,  see  [4mvw(1).[24m   All
       input files are piped through a preprocessor much like the C preproces-
       sor.  Files on the command line, or in "are interpreted  as  Synchonous
       Verilog, and are translated to SMV by [4mvl2smv(1).[0m

       If  [1m-check  [22mswitch  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, specifying the the truth value of the assertion  and
       if  false,  a  [1mcounterexample [22mshowing 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 verified. Property-spe-
       cific 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  com-
       mand 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 "For-
       wardSearch=0". For non-boolean options, the option value  is  the  next
       word  in  the  command line. For example, "-v 1" is equivalent to "Ver-
       bose=1".



[1mOPTIONS[0m
       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.

       [1m--     [22mDo not use the default options.

       [1m-abs [4m[22mfilename[0m
              Specifies the abstraction file.

       [1m-absref[0m
              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.

       [1m-bmc   [22mUse bounded model checking. This technique searchs for  a  coun-
              terexample  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.

       [1m-check [4m[22mname[0m
              Check  the  named  assertion.  If  a structure is specified, all
              assertions contained in that structure are checked.

       [1m-de    [22mUse conjunctive decompositions in model checking.

       [1m-D[4m[22msymbol=value[0m
              Define a symbol for the preprocessor, as in cc.

       [1m-enum  [22mEnumerate unknown values. This prevents propatation of  "unkown"
              values by introducing combinatinal variables.

       [1m-f     [22mCompute  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.

       [1m-foo [4m[22mfilename[0m
              Output final variable order (after model checking  and  sifting)
              to file filename.

       [1m-fsift [22mSift  just  once, after all properties checked. Useful only with
              -foo.

       [1m-I[4m[22mpathname[0m
              Look in directory "pathname" for include files, as in cc.

       [1m-i [4m[22mvariable-order-file[0m
              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.

       [1m-l [4m[22mlength[0m
              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.

       [1m-lazy  [22mOnly compile module instances on demand. This can speed up load-
              ing  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.

       [1m-m [4m[22mmodule-name[0m
              Treat the named module as the main module.

       [1m-nopr  [22mDo not used partitioned transition relations.

       [1m-nocp  [22mDo not use conjunctive partitioning of the transition relation.

       [1m-nodp  [22mDo not use disjunctive partitioning of the transition relation.

       [1m-o [4m[22mvariable-order-file[0m
              Output  the  variable  BDD  variable order to the given file and
              stop without checking any assertions. See also -i option.

       [1m-persist[0m
              Keep checking properties even after one is found to be false.

       [1m-pf [4m[22mnumber[0m
              Profile any BDD's larger than the given number of nodes.

       [1m-run [4m[22mtrace-file[0m
              Run a the simulation trace described in the given  file.  Format
              of this file is described below under SIMULATION.

       [1m-sif   [22mUse external model checker via the SIF interface (see below).

       [1m-sifliveness[0m
              The external solver supports liveness checking.

       [1m-sifsolver [4m[22msolver[0m
              Use solver as the external model checker.

       [1m-sift  [22mUse sifting to attempt to improve the variable order.

       [1m-smcsat2[0m
              Use  SAT-based  model  checking  (version  2).  Like proof-based
              abstraction, this technique is most effective when  large  parts
              of  the  system  being verified are not relevant to the property
              being verified. If you are suffering from  BDD  explosion  using
              -absref, you may want to try this.

       [1m-stubs [4m[22mfilename[0m
              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 rele-
              vant to the assertions being checked.

       [1m-together[0m
              Check all properties in a  property  group  in  the  same  model
              checker  run.  This  means  that the transition relation and the
              reached state set will be computed only once for the group.

       [1m-v [4m[22mnumber[0m
              A non-zero value causes a transcript of the run to be printed on
              the standard output. Higher numbers cause more output.

       [1m-Z     [22mInitialize  any  uninitialized  state variables to zero. This is
              useful for large codes translated from verilog that do not  ini-
              tialize registers. It is also completely bogus.


[1mTHE OPTIONS FILE[0m
       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.


[1mABSTRACTION FILES[0m
       When  verifying a given property, you can use definitions of signals at
       a chosen level of abstraction. This defines the "environment" for veri-
       fying 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 verifying 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 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 def-
       inition  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.


[1mPROPERTY GROUPS FILE[0m
       The  file "file.groups" is used to define groups of properties 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].


[1mVARIABLE ORDERING[0m
       Smv  uses  Binary  Decision Diagrams (BDDs) to represent sets and rela-
       tions in the model checking algorithm.  A BDD is a  decision  tree,  in
       which  variables  always  appear  in the same order as the tree is tra-
       versed 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  vari-
       ables  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 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 transition relation.  It is very important to minimize this number.
       Iterations are used to solve the fixed point equations which character-
       ize the various temporal operators, and also to search for counterexam-
       ples.  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.


[1mVARIABLE ORDER FILE[0m
       A variable order file specifies the initial order  for  the  BDD  vari-
       ables.  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 cur-
       rently only with the -de option,  which  uses  "conjunctive  decomposi-
       tions".   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  bool-
       ean). This is useful to know in case you are editing an order file out-
       put from smv.


[1mSIMULATION[0m
       A simultation trace file is a sequence of assignments to program  vari-
       ables. Each of these assignments overrides the value of the given vari-
       ables 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
       particular 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 [4mvw(1).[0m



[1mUSING VW WITH XEMACS[0m
       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 versions.


[1mCOMPATIBILITY WITH CARNEGIE MELLON SMV[0m
       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:
       [1m<name>[4m[22m:[24m[1mSPEC[4m[22m<formula>;[24m  In general, however, constructs from the current
       language and the original Carnegie Mellon  version  may  not  be  mixed
       within a single module.


[1mINTERFACING TO AN EXTERNAL MODEL CHECKER[0m
       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.


[1mSEE ALSO[0m
       [1mvw(1),[22mvl2smv(1)
       [1mK.[22mL.[1mMcMillan,[22mThe SMV language
       [1mKenneth L. McMillan, [4m[22mSymbolic[24m [4mModel[24m [4mChecking,[24m [1mKluwer, 1993.[0m


[1mBUGS[0m
       See the relase notes.




[1mAUTHOR[0m
       Kenneth L. McMillan, Cadence Berkeley Labs
       mcmillan@cadence.com




SMV (Cadence version)             23 Jan 1996                           SMV(1)
