Next: Choosing a search procedure Up: Translating an expression to Previous: Interconnect synthesis in reconfigurable   Contents

### 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  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 K 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.

For example, consider a simple 2-bit counter whose outputs are represented by variables (LSB) and (MSB). Introduce variables and whose values are intended to be the same as those of variables and , respectively, on the th time step. Suppose the starting state is the case where both and 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:

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:

2. Express the starting state:

3. Force legal transitions (repetitions of the transition relation):

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

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 and , , 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 ). The constraints are shown in canonical form in Figure .

Next: Choosing a search procedure Up: Translating an expression to Previous: Interconnect synthesis in reconfigurable   Contents
John Franco 2011-09-15