INTERFACING SMV TO EXTERNAL MODEL CHECKERS
------------------------------------------

SMV can be made to use an external model checker using the command
line switch "-sif". The model checking problem generated by SMV is
described in the SIF format. SMV executes the external model checker
with two arguments, as follows:

     solver file.sif file.out

where "solver" is the command name of the external solver, "file.sif"
is the input file for the model checker and "file.out" is the output
file. The solver command name is given by the SMV option "-sifsolver".
Thus, a typical SMV command line to use an external model checker
would be as follows:

      smv -sif -sifsolver mychecker file.smv

In addition, the switch "-sifliveness" can be used to indicate that
the external solver supports checking liveness properties (using the
SIF construct INFINITELY_OFTEN, described below). Without this switch,
all liveness properties are translated to safety properties, a process
which is likely to cause great inefficiency in BDD-based model
checkers, but is mostly harmless for bounded model checkers.

The SIF format
==============

The subset of SIF used by SMV is summarized here. SIF is more fully
described in the document "Documentation of the SIF file format".

Synopsis:

module <module_name>;

INPUT <input_name>;             -- input signal declaration
...

ZERO <net_name>;                -- assign zero to named net
...

<net_name> = <expr>;            -- assign expression to named net
...

STATE_PLUS <name> [<net>]       -- delay element, with initial value = net
...

STATE_PLUS <name> = <expr>      -- assign expression to delay element input
...

TEST <net>                      -- property: false if <net> is ever one
...

INFINITELY_OFTEN <name> <n1> & ... & <cn>
                                -- property: false if nets  c1..cn
				   true infinitely often


end

------------------


<expr>  ::  ( <expr> )  |  <expr> & <expr>  |  ^<expr>

------------------

Notes:

1) The order of declarations between module and end is irrelevant.

2) All nets are boolean valued.

3) The & symbol is "and", the ^ symbol is "not". There is no "or"
operator.  Use DeMorgan's laws to get "or".

4) There are no constants allowed in expreesions. Use the ZERO
delcaration to generate a zero constant, and negation to generate a
one constant.

5) In .sif, net names can contain any characters if enclosed in single
quotes ''. However, SMV only generates names of the form
[A-Za-z][A-Za-z0-9]* and does not use quotes.


External model checker output format
====================================

External model checkers should use the same format for output that SMV
uses in its .out files:


{
  ""                        -- description field = empty string
  {<test_name>}             -- net name of TEST
  <truth_value>             -- 1 if property true, 0 if false
  0                         -- loopback state -- not used
  0                         -- time field -- not used
  {                         -- trace (only if truth_value = 0)
    { <state> } 
    ...
    { <state> }
  }
}

where:

<state>  ::  <net> = <value> , ... , <net> = <value>

-----------

notes:

1) only the values of delay elements and inputs need be reported in
the trace

-----------


Variable encodings
==================

In .sif files generated from SMV, all the "multivalued" variables
(i.e., non-booleans) are encoded using boolean variables. Also, names
of variables are changed to a simple alphanumeric format to avoid
clashes in naming styles between different tools and reduce the file
size. That means that even the boolean variables do not have the same
names as in the original source files.

An external model checker that needs to know the names and binary
encodings of the original variables (for example, to print some
entertaining information for the user) may refer to the encoding file
generated by SMV.

The name of this file is indicated by the environment variable
SIF_ENCODING_FILE, which is set by SMV.

The format of this file is as follows:

<encoding> ... <encoding>

where:

<encoding> ::  {
                  <orig_var>
	          { <enc_var1> ... <enc_varn> }
		  {
		     { <enc_val> <orig_val> }
		     ...
		     { <enc_val> <orig_val> }
                  }
               }


<enc_val>  :: { <bool_val> ... <bool_val> }

-----------
notes:

1) <orig_var> is the name of a variable in the source files.

2) <enc_var1> ... <enc_varn> is the vector of boolean variables
encoding <orig_var>.

3) <enc_val> is a vector of boolean values encoding the original value
<orig_val>.

4) <orig_var> and <orig_val> is are arbitrary text strings not
containing white space.

5) There may be more than one encoding of a given <orig_val>, for a
given <orig_var>, and one encoding may correspond to more than one
<orig_val> due to abstraction.

6) TO INFER *ANYTHING* ABOUT THE REACHABLE STATE SPACE OR THE
TRANSITION RELATION FROM THE ENCODING FILE IS AN ERROR. This file is
*only* to be used for reporting information of a heuristic nature to
the user. It contains NO semantic information.  You really cannot
infer *any* information about what encodings may or be not be
reachable from this file. Really. Just don't go there. You are warned.


Time limits
===========

SMV is aware of the soft CPU time limit placed on it by the
setrlimit(2) mechanism of Unix. It in turn uses setrlimit(2) to set
the soft CPU time limit of the external model checker to reflect the
CPU time remaining when the external model checker is executed.

The ordinary behavior of a process when the CPU time limit is reached
is to exit on the signal SIGXCPU. SMV detects this and reports a
timeout accordingly.

However, if the external model checker is wrapped in a script (or
other parent process), the script must recognize that a timeout in the
model checker has occurred and report this fact to SMV via its exit
code. It is acceptable for a shell script simply to return the exit
code produced by the external model checker directly (as obtained from
$?). If for any other reason it is desired to indicate a timeout, this
can be accomplished by returning the exit code 128+SIGXCPU (note, the
value of SIGXCPU is defined <signal.h>.

Abnormal exits and the standard channels
========================================

The external model checker can indicate an abnormal termination
condition by returning a non-zero exit code. In this case, some
explanatory message should be printed to stderr. OTHERWISE, NOTHING
SHOULD BE OUTPUT ON STDERR. Any output intended as entertainment
for the user should be directed to stdout.