# Sequential Symbolic Model Generator. SSMG.

March 2007: This web page is being updated at the moment

Recent developments in SAT solvers and model checkers have allowed supposedly exponential-time problems to be solved and checked in practice. Here we suggest that a new tool is needed for system synthesis: The SSMG, (Sequential Symbolic Model Generator) finds solutions to problems phrased in terms of next state functions.

Most SAT solvers require CNF input, but converting to this leads to an explosion of terms in itself. Certain SAT solvers can accept arbitrary logic expressions, such as the one from prover.com (Stalmark) or those based on the method of [GIU99]. However, when we consider projection through the next state function, as implemented in our HPRLS project, another form of exponential blow-up is experienced.

What is required for our approach to system synthesis is a SAT-like solver, that generates solutions, but where the problem is phrased in terms of a number of free (or partially constrained) variables and their nth-power next state functions. The solution is valid for all settings of the free variables. This problem lies between SAT and generalised QBF (quantified boolean formula) problems.

## SSMG

SSMG is a program that accepts the following input:

• F: List of variables to be universally quantified

• X: List of fuse variables, for which a SAT solution must be found,

• A: Conjunction of assertions (properties of the model) that must be always satisifed,

• I: Conditions on the initial values of any variables,

• D: Next state definitions of certain variables.

Hence, its input is rather like that of a model checkers except for the presence of the list X of fuse variables. The job of SSMG is to find a setting of the fuse variables such that the assertions, A, are all always satisfied. SSMG input can either be an extended DIMACS file or in the form of basic ASCII declarations and logic equations.

SSMG can be used without next-state declarations, D, as a basic combinational SAT solver. Even without referring to the next-state of variables, our DIMACS extensions allow two new classes of variable to be defined. Firstly, we allow the user to list variables that cannot be the basis of a useful case split. Secondly, we allow the user to list variables that must be universally quantifed. An existential solution found for the remaining variables (SAT solution) must be valid for all settings of the universally quantifed variables. Finally, one does not have to use CNF or DIMACS at all because the equation form of input can be used.

A conventional model checker cannot be used to generate this solution by handing it the negation of A, since the counter example it produces will be valid for only one setting of F, whereas the SSMG generates a solution that satisfies A for all settings of F.

## Implementation

The BV1 implementation of SMGG will be described in the white paper HERE. The SAT part of this implementation uses a Davis-Putman core where case splits are selected by a small set of heuristics. Input is in the form of simple equations, or CNF if used purely as a SAT solver. Output is either a counter-example or a fuse mapping, expressed using simple XML. Mature sat-solver techniques, such as non-linear backtracking and recursive learning can be applied in future.

The DIMACS CNF input file supports a couple of extensions to facilitate input from external tools that support universal quantification in their conversion to CNF.

A relation D is formed, that relates the current and next states D(q, q'). D typically contains most of the sat fuses whose value we must find, but equally these may occur in I or A.

We use the following procedure to generate the model:

• 1. Set the current state predicate Q to be be the conjunction of the initial state restrictions I.

• 2. Form A(Q) and check for any fuse settings this requires (i.e. absolutely requires to be satisfiable). These settings are permanently part of our output. If the expression is clearly unsatisfiable, stop with an error. We then refine A, Q and D under those settings to get A', Q' and D'.

• 3. Rename Q' as Q, A' as A and D' as D, discarding the old definitions.

• 4. As in normal model checking, project Q forward through D to achieve Q'.

• 5. If Q is not the same as Q' then replace Q with the disjunction of Q' and Q and goto step 2.

• 6. SAT solve Q in the normal way.

## User Manual

The program is run from the command line and is normally called `ssmg' and this should be followed by any options and then the source file name.

```
ssmg  [ options ] srcfilename
```

Example CNF run

```
\$ ./ssmg -o spool -c  /homes/djg/bcd/hgen5-v100-s2029002754.cnf
CBG SSMG Version BV1.12
CNF input: Found 0 unit clauses, 709 non-trivial clauses
dp starting
******** FOUND
Solution found ok
Checker: 709 satisifed clauses out of 709.  79 fuses unbound.
```

The output file is in XML format. Here is an example example output. Only one solution is returned. The algorithm we use can result in a fuse being set to 0, 1 or X, although there is no guarantee that all possible X's are included in the result. There were 79 unset fuses in this example solution.

The '-o fn' command line option causes output to be written to a file. Without this the output is to the screen.

The '-v' command line flag causes verbose output. Capital V is more verbose still.

The '-c' command line flag causes the input file to be read as a standard CNF file instead of being parsed by yacc in the expression language.

The sets X and F of variables may be defined by default rules or by declarations in the input file. The default rules are that any variable that begins with 'x' defaults to being a fuse variable. Any other variable that is not given an initial value or a next state function is a free initially or thereafter respectively. External inputs to the system are modelled in this way.

The '-x' command line flag allows one to change the default prefix for sat fuse variables. The default is that all variables begining with 'x' must be found values that make all of the model properties hold. However, '-x doh' would cause all variables begining with 'doh' to become sat fuses instead.

## Extended CNF input file format.

A standard DIMACS CNF file contains a line

```
p cnf atoms clauses
```
followed by the CNF data. Such data can be solved for SAT by SSMG, and so SSMG can be used as a normal sat solver.

We extend the CNF file format by allowing a number of the atoms to be considered to be universally quantified instead of solved for. These atoms are denoted by listing them on a line that starts with the letter U and ends with a zero. For example:

```
U  10 11 22 33 66 102 0
```

This is not be very useful for a normal SAT solver since one can normally miss out these atoms from all the clauses instead. It does make one difference in the case of a clause that is a trivial tautology. Specifically, if a clause contains both x and -x and x is then listed under U, the remainder of the tautological clause is exposed to influence the solution.

We also extend the CNF file format to allow a number of the atoms to be declared as `non-fuse' meaning they should not be used as the basis for a DP case split. There are two aspects two this. Firstly, where an intermediate variable is introduced during CNF conversion, then as reported in [GIU99], it is unneccesasry to consider such new variables during case split. For example

```
(A + B.C)
```
can be converted to CNF while preserving satisfiability as

```
(A + Y)(~Y + B)(~Y + C)
```
but there is no need to do a case split on the new variable Y.

Secondly, where a universally quantified variable is below the new variable Y, then Y needs to become a Skolem function. For example

```
\Ax.(A + x.C)
```
requires Y(x) to be introduced

```
\Ax.\Ey.(A + y)(~y + x)(~y + C)
=
\Ax.(A + Y(x))(~Y(x) + x)(~Y(x) + C)
```
If Y(x) is represented in the CNF file as just another literal, it is wrong to do a case split on that literal, since its value cannot be forced independently of other literals in the file.

Therefore, we introduce a second extension to the CNF file that allows such skolem literals to be identified and to be excluded as case split targets:

```
S  122 366 121 0
```
these literals are only used for resolution eliminations.

## Equations Input File Format and Expression Syntax

Non-CNF input must use the following syntax:

Comments are introduced with double slash

```
// This is a comment
```

Initial values of variables are given by assigning to I(x). More general starting conditions are introduce using the 'initial' statement.

```
I(variable) := exp;
initial exp;
```

Next state functions are given by assigning to X(x).

```
X(variable) := exp;
```

The only CTL quantifier implemented at the moment is `AG', meaning that all properties must hold along all paths leading to all reachable states. This is the only one I currently need.

Rather than using the string 'AG', model constraints are introduced with always or never and are true for the initial states and all reachable states. The two statements are interchangable by negating the expression. The conditions required to be true only in the initial state are introduced by any number of initial statements.

```
always exp;
never exp;
initial exp;
```

Macro or intermediate style definitions are given by assigning to a macro variable name

```
myvar := exp;
```

Boolean expressions may use the following operators with binding powers given on this page:H1OPERATORS.

```
~ ^ == !=  | & && || !  \/  /\  =>  <=>
```

Variables that are not assigned are assumed to be external inputs, free to change on any step, unless they start with the letter 'x' (or other string given on the command line).

Universal quantification is implied by default for all unconstrained values: i.e. the model generated must be true for all possible unconstrained initial value and external input patterns.