Bounded Model Checking

A sequential circuit differs from a combinational circuit in that output values depend not only on current input values but also on the history of change of those values. This may be modeled by a digraph such as the one in Figure 15 where each node represents a state of all output and intermediate values based on some input change history and each arc is labeled by input(s) whose changing value(s) cause(s) a transition from one state to another. Each transition is referred to below as a time step.

Let a circuit property be expressed as a propositional Boolean expression. An example of a property for a potential JK flip flop might be J $\wedge$ K $\wedge$ Q meaning that it is possible to have an output Q value of T if both inputs J and K have value T.

The following time-dependent expressions are among those that typically need to be proved for a sequential circuit.

1. For every path (in a corresponding digraph) property P is true at the next time step.
2. For every path property P is true at some future time step.
3. For every path property P is true at every future time step.
4. For every path property P is true until property Q is true.
5. There exists a path such that property P is true at the next time step.
6. There exists a path such that property P is true at some future time step.
7. There exists a path such that property P is true at every future time step.
8. There exists a path such that property P is true until property Q is true.

To construct a Boolean expression which must have value T if and only if the desired time-dependent expression holds, the Boolean expression must have components which:

1. force the property or properties of the time dependent expression to hold,
2. establish the starting state,
3. force legal transitions to occur.

In order for the Boolean expression to remain of reasonable size it is generally necessary to bound the number of time steps in which the time-dependent expression is to be verified; hence, bounded model checking.

Figure 15: A state machine representing a sequential circuit

For example, consider a simple 2-bit counter whose outputs are represented by variables $v_1$ (LSB) and $v_2$ (MSB). Introduce variables $v^i_1$ and $v^i_2$ whose values are intended to be the same as those of variables $v_1$ and $v_2$, respectively, on the $i$th time step. Suppose the starting state is the case where both $v^0_1$ and $v^0_2$ have value 0. The transition relation is

Current Output		Next Output
00	:	01
01	:	10
10	:	11
11	:	00

which can be expressed as the following Boolean function:

$$(v^{i+1}_1 \equiv \neg v^i_1) \wedge (v^{i+1}_2 \equiv v^i_1\oplus v^i_2).$$

Suppose the time-dependent expression to be proved is:

Can the two-bit counter reach a count of 11 in exactly three time steps?

Assemble the propositional formula having value T if and only if the above query holds as the conjunction of the following three parts:

1. Force the property to hold:
   
   $$(\neg(v^0_1\wedge v^0_2)\wedge \neg(v^1_1\wedge v^1_2)\wedge \neg(v^2_1\wedge v^2_2)\wedge (v^3_1\wedge v^3_2))$$
   
   

2. Express the starting state:
   
   $$(\neg v^0_1\wedge \neg v^0_2)$$
   
   

3. Force legal transitions (repetitions of the transition relation):
   
   $$~~(v^1_1 \equiv \neg v^0_1) \wedge (v^1_2 \equiv v^0_1\oplus v^0_2)\wedge$$
   
   
   
   
   
   $$~~(v^2_1 \equiv \neg v^1_1) \wedge (v^2_2 \equiv v^1_1\oplus v^1_2)\wedge$$
   
   
   
   
   
   $$(v^3_1 \equiv \neg v^2_1) \wedge (v^3_2 \equiv v^2_1\oplus v^2_2)$$
   
   

The reader may check that the following satisfy the above expressions:

$$v^0_1=0, v^0_2=0, v^1_1=1, v^1_2=0, v^2_1=0, v^2_2=1, v^3_1=1, v^3_2=1.$$

This assignment can be found by running sbsat on the example file bmc_example.ite with the flag -R r. It may also be verified that no other assignment of values to $v^i_1$ and $v^i_2$, $0\leq i\leq 3$, satisfies the above expressions by running the previous command with two extra flags, namely -max-solutions 0 and -All 0 (details on these flags can be found in Section 7). The constraints are shown in canonical form in Figure 16.

Figure 16: Bounded model checking example in canonical form.