Bounded Model Checking Using Satisfiability Solving.
The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.
Figure

must cause the initial state to be visited infinitely often. While there is no particular reason a counter
should work this way, we use the example to illustrate how fairness constraints are imposed in bounded model
checking. Given such a fairness constraint, a counterexample to the liveness property AF(b^a) would then need
to include a transition to the (0;0) state. This is a path with a loop as before, but with the additional constraint that
:a ^:b has to hold somewhere on the loop. This changes the generated Boolean formula as follows. For each
backloop, T(s2;s3), where the state s3 is required to be equivalent to either s0, s1 or s2, we add a term that requires
:a^:b to hold on the loop. For example, for the possible loop from s2 to s0 (the case where s3 = s0), we would
replace
by
(a3
with ci defined as :ai ^:bi. As there is no counterexample that would satisfy this fairness constraint, in this case
the resulting propositional formula would be unsatisfiable.
3.4 Conversion to CNF
Satisfiability testing for propositional formulae in known to be an NP-complete problem, and all known decision
procedures are exponential in the worst case. However, they may use different heuristics in guiding their search
and, therefore, exhibit different average complexities in practice. Precise characterization of the hardness of a
certain propositional problem is difficult and is likely to be dependent on the specific decision procedure used.
Many propositional decision procedures assume the input problem to be in CNF (conjunctive normal form).
Usually, it is a goal to reduce the size of the CNF version of the formula, although this may not always reduce the
complexity of the search. Our experience has been, however, that reducing the size of the CNF does reduce the
time for the satisfiability test as well.
in CNF is represented as a set of clauses. Each clause is a set of literals, and each literal is either
a positive or negative propositional variable. In other words, a formula is a conjunction of clauses, and a clause is
a disjunction of literals. For example, ((a _:b _c) ^(d _:e)) is represented as ffa;:b;cg;fd;:egg. CNF is is
also referred to as clause form.
Given a Boolean formula f, one may replace Boolean operators in f with :;^ and _ and apply the distributivity
rule and De Morgan's law to convert f to CNF. The size of the converted formula can be exponential with
respect to the size of f, the worst case occurring when f is in disjunctive normal form. To avoid the exponential
explosion, we use a structure preserving clause form transformation [28].
procedure bool-to-cnf( f, vf )
f
case
cached( f) == v:
return clause(vf
return clause( f $ vf );
f == hg:
return clause(vf
Fig. 2. An algorithm for generating conjunctive normal form. f, g and h are Boolean formulas. v, vh and vg are Boolean
variables. '' represents a Boolean operator.

Figure

outlines our procedure. Statements which are underlined represent the different cases considered, the
assignment while the symbol == denotes equality. Given a Boolean formula f, bool-to-
returns a set of clauses C which is satisfiable if and only if the original formula, f, is satisfiable. Note
that C is not logically equivalent to the original formula, but, rather, preserves its satisfiability. The procedure
traverses the syntactical structure of f, introduces a new variable for each subexpression, and generates clauses
that relate the new variables. In Figure 2, we use symbols g and h to denote subexpressions of the Boolean
formula f, and we use vf , vg and vh to denote new variables introduced for f, g and h. C1 and C2 denote sets
of clauses. If a subexpression, q, has been cached, the call to cached(q) returns the variable vq introduced for
q. The procedure, clause(), translates a Boolean formula into clause form. It replaces Boolean connectives such
as implication, !, or equality, $, etc., by combinations of and, or and negation operators and subsequently
converts the derived formula into conjunctive normal form. It does this in a brute force manner, by applying the
distributivity rule and De Morgan's law. As an example, if u and v are Boolean variables, clause() called on u
returns ff:u;vg;fu;:vgg. It should be noted that clause() will never be called by bool-to-cnf with more than 3
literals, and so, in practice, the cost of this conversion is quite acceptable. If v, vh, vg are Boolean variables and
'' is a Boolean operator, v $ (vh vg) has a logically equivalent clause form, clause(vf $ vh vg), with no more
than 4 clauses, each of which contains no more than 3 literals.
Internally, we represent a Boolean formula f as a directed acyclic graph (DAG), i.e., common subterms of
f are shared. In the procedure bool-to-cnf(), we preserve this sharing of subterms, in that for each subterm in f,
only one set of clauses is generated. For any Boolean formula f, bool-to-cnf( f,true) generates a clause set C with
O(jfj) variables and O(jfj) clauses, where jfj is the size of the DAG for f.
In

Figure

2, we assume that f only involves binary operators, however, the unary operator, negation, can be
handled similarly. We have also extended the procedure to handle operators with multiple operands. In particular,
we treat conjunction and disjunction as N-ary operators. For example, let us assume that vf represents the formula
Vni=0 ti. The clause form for
is then:
ff:vf ;t0g;f:vf ;t1g;:::;f:vf ;tng;fvf ;:t0;:::;:tngg
If we treat ^ as a binary operator, we need to introduce n1 new variables for the subterms in Vni=0 ti. With this
optimization, the comparison between two registers r and s occurring as a subformula, V1i=50(r[i]
can be converted into clause form without introducing new variables.
4 Experimental Results
At Carnegie-Mellon University, a model checker has been implemented called BMC, based on bounded model
checking. Its input language is a subset of the SMV language [26]. It takes in a circuit description, a property to be
proven, and a user supplied time bound, k. It then generates the type of propositional formula described in Section
3.1. It supports both the DIMACS format [20] for CNF formulae, and the input format for the PROVER Tool [5]
which is based on Stalmarck's Method [35]. In our experiments, we have used the PROVER tool, as well as two
public domain SAT solvers, SATO [39] and GRASP [33], both of which use the DIMACS format.
We first discuss experiments on circuits available in the public domain, that are known to be difficult for BDD-based
approaches. First we investigated a sequential multiplier, the shift and add multiplier of [12]. We specified
that when the sequential multiplier is finished, its output is the same as the output of a certain combinational
multiplier, the C6288 circuit from the ISCAS'85 benchmark set, when the same input words are applied to both
multipliers. The C6288 multiplier is a 16x16 bit multiplier, but we only allowed 16 output bits as in [12], together
with an overflow bit. We checked the above property for each output bit individually, and the results are shown
in

Table

1. For BDD-based model checkers, we used a manually chosen variable ordering where the bits of the
registers are interleaved. Dynamic reordering, where the application tries to change reorderings on the fly, failed
to find a considerably better ordering in a reasonable amount of time. The proof that the multiplier is finished after
a finite number of steps involves the verification of a simple liveness property which can be checked instantly both
with BDD based methods and bounded model checking.
In [25] an asynchronous circuit for distributed mutual exclusion is described. It consists of n cells for n users
that want to have exclusive access to a shared resource. We proved the liveness property that a request for using
the resource will eventually be acknowledged. This liveness property is only true if each asynchronous gate does
not delay execution, indefinitely. This assumption is modeled by a fairness constraint (fairness constraints were
explained in Section 3.3). Each cell has exactly gates and therefore the model has n
bit
sec MB
sec MB
SATO
sec MB
PROVER
sec MB13579111315
43983 73
26
sum 71923 2202 23970 1066

Table

1. 16x16 bit sequential shift and add multiplier with overflow flag and 16 output bits.
where n is the number of cells. Since we do not have a bound for the maximal length of a counterexample for
the verification of this circuit we could not verify the liveness property completely, rather, we showed that there
are no counterexamples of particular length k. To illustrate the performance of bounded model checking we chose
5;10. The results can be found in Table 2.
We repeated the experiment with a buggy design, by simply removing several fairness constraints. Both
PROVER and SATO generate a counterexample (a 2 step loop) nearly instantly (see Table 3).
cells sec MB sec MB
SATO
sec MB
PROVER
sec MB
SATO
sec MB
PROVER
sec MB3579111315
4857
9 5
22 8
9 8
107 19
168 22
54 5
444 9

Table

2. Liveness for one user in the DME.
cells
sec MB
sec MB
SATO
sec MB
PROVER
sec MB3579111315
5622 38
segmentation
28
14 44
413 702
719 702

Table

3. Counterexample for liveness in a buggy DME.
5 Experiments on Industrial Designs
In this section, we will discuss a series of experiments on industrial designs, checking whether certain predicates
were invariants of these designs. First, we explain an optimization for bounded model checking that was used in
these experiments.
5.1 Bounded Cone of Influence
The Cone of Influence Reduction is a well known technique3 that reduces the size of a model if the propositional
formulae in the specification do not depend on all state variables in the structure. The basic idea of the Cone
of Influence (COI) reduction is to construct a dependency graph of the state variables in the specification. In
building the dependency graph, a state variable is represented by a node, and that node has edges emanating out to
nodes representing those state variables upon which it combinationally depends. The set of state variables in this
dependency graph is called the COI of the variables of the specification. In this paper, we call this the classical
COI, to differentiate it from the bounded version. The variables not in the classical COI can not influence the
validity of the specification and can therefore be removed from the model.
This idea can be extended to what we call the Bounded Cone of Influence. The formal definition for the
bounded COI is given in [4], and we give, here, an intuitive explanation. The intuition is that, over a bounded
time interval, we need not consider every state variable in the classical COI at each time point. For example, if
we were to check EF p, where p is a propositional formula, for a time bound of k = 0, we would need to consider
only those state variables upon which p combinationally depends. If the initial values for these were consistent
with p holding, then EF p would evaluate to true, without needing to consider any additional state variables in
the classical COI. Let us, for convenience, call the set of state variables upon which p combinationally depends
its initial support. If we could not prove EF p true for wanted to check it for would need to
consider the set of state variables upon which those in the initial support depend. These may include some already
in the initial support set, if feedback is present in the underlying circuit. Clearly, the set union of the initial support
set plus this second support set are the only state variables upon which the truth value of EF p depends for time
1. Again, this will always be a subset of the state variables in the entire classical COI. If we restrict
ourselves to expanding formula 1 of Section 3.1 only for those variables in the bounded COI for a particular k, we
will get a smaller CNF formula, in general, than if we were to expand it for the entire, classical COI. This is the
main idea behind the Bounded Cone of Influence.
3 The cone of influence reduction seems to have been discovered and utilized by a number of people, independently. We note
that it can be seen as a special case of Kurshan's localization reduction [23].
5.2 PowerPC Circuit Experiments
We ran experiments on subcircuits from a PowerPC microprocessor under design at Motorola's Somerset design
center, in Austin, Texas. While a processor is under design at Somerset, designers insert assertions into the register
transfer level (RTL) simulation model. These Boolean expressions are important safety properties, i.e., properties
which should hold at all time points. If an assertion is ever false during simulation, an immediate error is flagged. In
our experiments, we checked, using BMC and two public domain SAT checkers, SATO and GRASP, 20 assertions
chosen from 5 different processor design blocks. We turned each into an AG p property, where p was the original
assertion. For each of these, we:
1. Checked whether p was a tautology.
2. Checked whether p was otherwise an invariant.
3. Checked whether AG p held for various time bounds, k, from 0 to 20.
The gate level netlist for each of the 5 design blocks was translated into an SMV file, with each latch represented
by a state variable having individual next state and initial state assignments. For the latter, we assigned the 0
or 1 values we knew the latches would have after a designated power-on-reset sequence4 Primary inputs to design
blocks were modeled as unconstrained state variables, i.e., having neither next state nor initial state assignments.
For combinational tautology checking we eliminated all initialization statements and ran BMC with a bound of
checking the inner, propositional formula, p, from each of the AG p specifications. Under these conditions,
the specification could hold only if p was true for all assignments to the state variables in its support.
Invariance checking entails checking whether a propositional formula holds in all initial states and is preserved
by the transition relation, the latter meaning that all successors of states satisfying the formula also satisfy it.
If these conditions are met, we call the predicate an inductive invariant. We ran BMC on input files with all
initialization assignments intact, for each design block and each p in each AG p specification, with a time bound
of determined whether each formula, p, held in the single, valid initial state of each design. We then
ran BMC in a mode in which, for each design block and each AG p specification, all initialization assignments
were removed from the input file, and, instead, an initial states predicate was added that indicated the initial
states should be all those states satisfying p. Note that we did not really believe the initial states actually were
those satisfying p. This technique was simply a way of getting the BMC tool to check all successors of all states
satisfying p, in one time step. The time bound, k, was set to 1, and the AG p specification was checked. If the
specification held, this showed p was preserved by the transition relation, since AG p could only hold, under these
circumstances, if the successors of every state satisfying p also satisfied p. Note that AG p not holding under these
conditions could possibly be due exclusively to behaviors in unreachable states. For instance, if an unreachable
state, s, existed which satisfied p but had a successor, s0, which did not, then the check would fail. Therefore,
because of possible bad behaviors in unreachable states, this technique can only show that p is an invariant, but
cannot show that it is not. However, we found this type of inductive invariance checking to be very inexpensive
with bounded model checking, and, therefore, very valuable. In fact, we made it a cornerstone of the methodology
we recommend in Section 6.
In these experiments, we used both the GRASP [33] and SATO [38] satisfiability solvers. When giving results,
however, we do not indicate from which solver they came, rather, we just show the best results from the two. There
is actually an interesting justification for this. In our experience, the time needed for satisfiability solving is often
just a few seconds, and usually no more than a few minutes. However, there are problem instances for which a
particular SAT tool will labor far longer, until a timeout limit is reached. We have quite often found that when
one SAT solving tool needs to be aborted on a problem instance, another such tool will handle it quickly; and,
additionally, the same solvers often switch roles on a later problem instance, the former slow solver suddenly
becoming fast, the former fast one, slow. Since the memory cost of satisfiability solving is usually slight, it makes
sense to give a particular SAT problem, in parallel, to several solvers, or to versions of the same solvers with
different command line arguments, and simply take the first results that come in. So, this method of running
multiple solvers, as we did, on each job, is something which we recommend.
The SMV input files were given to a recent version of the SMV model checker (the SMV1version referred
to earlier) to compare to BDD based model checking. We did 20 SMV runs, checking each of the AG p specifi-
cations, separately. When running SMV, we used command line options that enabled the early detection, during
4 Microprocessors are generally designed with specified reset sequences. In PowerPC designs, the resulting values on each
latch are known to the designers, and this is the appropriate initial state for model checking.
reachability analysis, of false AG p properties. In this mode, the verifier did not need to compute a fixpoint if a
counterexample existed, which made the comparison to BMC more appropriate. We also enabled dynamic variable
ordering when running SMV.
All experiments were run with wall clock time limits. The satisfiability solvers were given 15 minutes wall
clock time, maximum, to complete each run, while SMV was given an hour for each of its runs. BMC, itself, was
never timed, as its task of translating the design description and the specification is usually done quite quickly.
The satisfiability solving and SMV runs were done on RS6000 model 390 workstations, having 256 Megabytes
of local memory.
5.3 Environment Modeling
We did not model the interfaces between the subcircuits on which we ran our experiments and the rest of the
microprocessor or the external computer system in which the processor would eventually be placed. This is commonly
referred to as environment modeling. One would ideally like to do environment modeling on subcircuits
such as we experimented on, since these are not closed systems. Rather, they depend for their correct functioning
upon input constraints, i.e., certain input combinations or sequences not occurring. The rest of the system
must guarantee this [21]. However, in the type of invariant checking we did, one would always be assured of
true positives, since if a safety property holds with a totally unconstrained environment, then it holds in the real
environment (this is proven in [13, 18]).
It is likely that an industrial design team would first check safety properties with unconstrained environments,
since careful environment modeling can be time consuming. They would then decide, on an individual basis, what
to do about properties that failed: invest in the environment modeling for more accurate model checking, in order
to separate false failures from real ones, or hope that digital simulation will find any real violations that exist.
Importantly, the model checker's counterexamples could provide hints as to which simulations, on the complete
design not just the subcircuit, may need to be run. For instance, the counterexample may indicate that certain
instructions need to be in execution, certain exceptions occurring, etc. The properties that pass the invariance test
need no more digital simulation, and thus conserve CPU resources.
In the examples we did run, all the negatives proved, upon inspection with designers, to be false negatives.
The experiments still yield, however, useful information on the capacity and speed of bounded model checking.
Further, in Section 6, we describe a methodology that can reduce or eliminate false negatives.
5.4 Experimental Results
As mentioned, we checked 20 safety properties, distributed across 5 design blocks from a single PowerPC micro-
processor. These were all control circuits, having little or no datapath elements. Their sizes were as follows:
Circuit Latches PIs Gates
bbc 209 479 4852
ccc 371 336 4529
cdc 278 319 5474
dlc 282 297 2205
Circuit Spec Latches PIs
dlc 7 119 153

Table

4. Before and After Classical COI Primary Inputs)
In table 4, we report the sizes of the circuits before and after classical COI reduction has been applied.
Each AG p specification is given an arbitrary numeric label, on each circuit. These do not relate specifications on
different design blocks, e.g., specification 2 of dlc is in no way related to specification 2 of sdc. Many properties
involved much the same cone of circuitry on a design block, as can be seen by the large number of specifications
having cones of influence with the same number of latches and PIs. However, these reduced circuits were not
identical, from one specification to another, though they shared much circuitry.

Table

5 gives the results of tautology and inductive invariance checking for each p from each AG p specifica-
tion. These runs were done with bounded COI enabled. There are columns for tautology checking, for preservation
by the transition relation and for preservation in initial states. The last two conditions must both hold for a Boolean
formula to be an inductive invariant. AY in the leftmost part of a column indicates the condition holding, an
N that it does not, When a Y is recorded, time and memory usage may appear after it, separated by slashes.
These are recorded only for times 1 second, and memory usage 5 megabytes, otherwise a - appears for
insignificant time and memory. As can be seen, tautology and invariance checking can be remarkably inexpensive.
This is an extremely important finding, as these can be quite costly with BDD based methods, and are at the heart
of the verification methodology we propose in Section 6.
We were surprised by the small number of assertions that were combinational tautologies. We had expected
that designers would try to insure safety properties held by relying on combinational, as opposed to sequential
circuitry. However, the real environment may, in fact, constrain inputs to design blocks combinationally such that
these are combinational tautologies. See Section 6 for a discussion of this.
As stated above, many of our examples exhibited false negatives, and they did so at low time bounds. Other
of our examples were found to be inductive invariants. Satisfiability solving went quickly at high values of k if
counterexamples existed at low values of k or if the property was an invariant. The more difficult SAT runs are
those for which neither counterexamples nor proofs of correctness were found. Table 6 shows the four examples
which were of this type, bbc specs 1, 3 and 4, and sdc spec 1. All results, again, were obtained using bounded
COI. We also ran these examples using just classical COI, and we observed that the improvement that bounded
COI brings relative to classical COI wears off at higher k values, specifically, at values near to 10. Intuitively, this
is due to the fact that, as we extend further in time, we eventually compute valuations for all the state variables in
the classical cone of influence. However, since we expect bounded model checking to be most effective at finding
short counterexamples, bounded COI is helping augment the system's strengths.
In table 6, long k is the highest k value at which satisfiability solving was accomplished, and vars and
clauses list the number of literals and clauses in the CNF file at that highest k level. The time column gives
CPU time, in seconds, for the run at that highest k value. Regarding memory usage, this usually does not exceed
a few tens of megabytes, and is roughly the storage needed for the CNF formula, itself.

Table

7 lists the circuits and specifications which were either shown to be inductive invariants or for which
counterexamples were found. Under the column holds, a Y indicates a finding of being an inductive invariant,
a N the existence of a counterexample. For the counterexamples, the next column, fail k, gives the value of
k for which the counterexample was found. Since all counterexamples were found with k values 2, we did not
list time and memory usage, as this was extremely slight. In each case, the satisfiability solving took less than a
second, and memory usage never exceeded more than 5 megabytes.
Lastly, the results of BDD-based model checking are that SMV was given each of the 20 properties separately,
but completed only one of these verifications. The 19 others all timed out at one hour wall clock time. SMV was
run when the Somerset computer network allowed it unimpeded access to the CPU it was running on; and still,
under these circumstances, SMV was only able to complete the verification of sdc, specification 3. Classical COI
for this specification gave a very small circuit, having only 23 latches and 15 PIs. SMV found the specification
false in the initial state, in approximately 2 minutes. Even this, however, can be contrasted to BMC needing 2
seconds to translate the specification to CNF, and the satisfiability solver needing less than 1 second to check it!
5.5 Comparison to BDD Based Model Checking
It is useful to reflect on what the experiments on PowerPC microprocessor circuits show and what they do not.
First, the experiments should not be interpreted as evidence that BDD based model checkers cannot handle circuits
of the size given. There are approximation techniques, for instance where certain portions of a circuit are deleted
or approximated with simpler Boolean functions that still yield true positives for invariance checking, and these
could have been employed. Some of the verifications may have gone through under these circumstances. However,
the experiments, as run, do give a measure of the size limits of BDD based and SAT based model checking.
input constraints it proved easy to reach states that violated the purported invariants. It has been
noted, empirically, by many users of BDD based tools, that it is much harder to build BDDs for incorrect designs
than it is for correct designs. There is no theoretical explanation of why this is so, but it may very well be that
Circuit Spec Tautology Tran Rel'n Init State
dlc 6 N - N - Y -

Table

5. Tautology and Invariance Checking Results
circuit spec long k vars clauses time

Table

6. Size Measures for Difficult Examples
circuit spec holds fail k
dlc
dlc 6 N 2
dlc 7 N 0

Table

7. Invariants and Counterexamples
SMV, or another BDD based model checker, could have successfully completed many of the property checks on
versions of these designs having accurate input constraints. However, in a way this is to the credit of bounded
model checking, in that it seems able to handle problem instances which are difficult for BDDs.
another observation is that when a design has a large number of errors, random, digital simulation can
find counterexamples quickly. Many commercial formal verification tools first run random digital simulations
on a design, to see if property violations can be detected easily. While we did not do this in our experiments,
we feel it is likely this, too, would have found quick counterexamples. However, this only shows that bounded
model checking is at least as powerful as this method, on buggy designs-yet, bounded model checking has the
additional capability of conducting exhaustive searches, within certain limits.
As to those limits, a big question with bounded model checking is whether it can, or will, find long coun-
terexamples. Clearly, it is to the advantage of BDD based model checking that if the BDDs can be built and
manipulated, all infinite computation paths, i.e., all loops through the state graph, can be examined. But, all too
often, as mentioned, the BDDs cannot be built or manipulated. In those cases, even if bounded model checking
cannot be run over many time steps, it does give exhaustive verification at each time step, and certainly is worth
running. Most of our experiments did not produce information that would answer the question as to the expected
length of counterexamples, but a few did. Out of the verifications attempted, 4 yielded neither counterexamples
nor proofs of correctness, and simply timed out. This means for the property being checked, these designs were
not buggy, up to the depth checked. Of these four, bbc specs 1, 3 and 4, sdc spec 1, BMC was able to go out to
4, 10, 5 and 4 time steps, respectively (see table 6). Thus, we expect that with current technology, we might be
limited to between 5 and time steps on large designs. Of course, we could have let the SAT tools run longer,
and undoubtedly we would have extended some of these numbers. But, that was not the goal of our experiment.
We tried to see what one could expect running large numbers of designs through a verifier, where not much time
could be spent on any individual verification, as we felt this would replicate conditions that would occur in indus-
try. Still even if we end up limited, in the end, to explorations within 5 to 10 time steps of initial states, if such
explorations can be done quickly and are exhaustive, it is certain they will aid in finding design errors in industry.
And, of course, we hope to extend these limits by further research.
Lastly, the results for invariance checking speak for themselves. We believe the performance would only
improve given accurate input constraints. There is no logical reason to believe otherwise. Yet, it is hard to improve
on the existing performance, since nearly every invariance check completed in under 1 second!
6 A Verification Methodology
Our experimental results lead us to propose an automated methodology for checking safety properties on industrial
designs. In what follows, we assume a design divided up into separate blocks, as is the norm with hierarchical
VLSI designs. Our methodology is as follows:
1. Annotate each design block with Boolean formulae required to hold at all time points. Call these the block's
inner assertions.
2. Annotate each design block with Boolean formulae describing constraints on that block's inputs. Call these
the block's input constraints.
3. Use the procedure outlined in Section 6.2 to check each block's inner assertions under its input constraints,
using bounded model checking with satisfiability solving.
This methodology could be extended to include monitors for satisfaction of sequential constraints, in the
manner described in [21], where input constraints were considered in the context of BDD based model checking.
6.1 Incorporating Constraints
Let us consider propositional input constraints with which the valuations of circuit inputs must always be consistent

We discussed Kripke structures in Section 2, and how these can be used to model digital hardware systems.
We defined the unrolled transition relation of a Kripke structure in formula 1, of Section 3.1. We can incorporate
input constraints into the unrolled transition relation as shown below, where we assume the input constraints are
given by a propositional formula, c, over state variables representing inputs.
Below, when we speak of checking invariants under input constraints, we mean using formula 2 in place of
formula 1 for the unrolled transition relation, [ M ] ,
6.2 Safety Property Checking Procedure
The steps for checking whether a block's inner assertion, p, is an invariant under input constraints, c, are:
1. Check whether p is a combinational tautology in the unconstrained K, using formula 1. If it is, exit.
2. Check whether p is an inductive invariant for the unconstrained K, using formula 1. If it is, exit.
3. Check whether p is a combinational tautology in the presence of input constraints, using formula 2. If it is,
go to step 6.
4. Check whether p is an inductive invariant in the presence of input constraints, using formula 2. It it is, go to
step 6.
5. Check if a bounded length counterexample exists to AG p in the presence of input constraints, using formula 2.
If one is found, there is no need to examine c, since the counterexample would exist without input constraints5.
If a counterexample is not found, go to step 6. The input constraints may need to be reformulated and this
procedure repeated from step 3.
6. Check the input constraints, c, on pertinent design blocks, as explained below.
Inputs that are constrained in one design block, A, will, in general, be outputs of another design block, B. To check
A's input constraints, we turn them into inner assertions for B, and check them with the above procedure. One must
take precautions against circular reasoning while doing this. Circular reasoning can be detected automatically,
however, and should not, therefore, be a barrier to this methodology.
The ease with which we carried out tautology and invariance checking indicates the above is entirely feasible.
Searching for a counterexample, step 5, may become costly at high k values; however, this can be arbitrarily
limited. It is expected that design teams would set limits for formal verification and would complement its use
with simulation, for the remainder of available resources.
Conclusions
We can summarize the advantages of bounded model checking as follows. Bounded model checking entails only
slight memory and CPU usage, especially if the user is willing to not push the time bound, k, to its limit. But there
are some encouraging results for larger values of k as well [32]. The technique is extremely fast for invariance
checking. Counterexamples and witnesses are of minimal length, which make them easy to understand. The
technique lends itself well to automation, since it needs little by-hand intervention. The disadvantages of bounded
model checking are that, at present, the implementations are limited as to the types of properties that can be
checked, and there is no clear evidence the technique will consistently find long counterexample or witnesses.
From this discussion it follows that at the current stage of development bounded model checking alone can not
replace traditional symbolic model checking techniques based on BDDs entirely. However in combination with
traditional techniques bounded model checking is able to handle more verifications tasks consistently. Particularly
for larger designs where BDDs explode, bounded model checking is often still able to find design errors or as in
our experiments violations of certain environment assumptions.
Since bounded model checking is a rather recent technique there are a lot of directions for future research:
1. The use of domain knowledge to guide search in SAT procedures.
2. New techniques for approaching completeness, especially in safety property checking, where it may be the
most possible.
3. Combining bounded model checking with other reduction techniques.
5 This is implied by the theorems in [13, 18], mentioned in Section 5.2
4. Lastly, combining bounded model checking with a partial BDD approach.
The reader may also refer to [32], which presents successful heuristics for choosing decision variables for SAT
procedures in the context of bounded model checking of industrial designs. In [37] early results on combining
BDDs with bounded model checking are reported. See also [1] for a related approach.
While our efforts will continue in these directions, we expect the technique to be successful in the industrial
arena as presently constituted, and this, we feel, will prompt increased interest in it as a research area. This is all
to the good, as it will impel us faster, towards valuable solutions.


--R


Automatic verification of finie-state concurrent systems using temporal logic specifcations
Verification of the Future- bux+ Cache Coherence Protocol
Model Checking and Abstraction.
Model Checking and Abstraction.
Model Checking.
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams.
A Computing Procedure for Quantification Theory.
Building Decision Procedures for Modal Logics from Propositional Decision Procedures - the case study of modal
Model Checking and Modular Verification.
An Intermediate Design Language and its Analysis.
The second DIMACS implementation challenge
Design constraints in symbolic model checking.
Pushing the envelope: Planning

Test Generation using Boolean Satisfiability.
The design of a self-timed circuit for distributed mutual exclusion
Symbolic Model Checking: An Approach to the State Explosion Problem.
A Computational Theory and Implementation of Sequential Hardware Equivalence.
A structure-preserving clause form translation
Specification and Verification of Concurrent Systems in CESAR.
Analyzing a PowerPC 620 Microprocessor Silicon Failure using Model Checking.
Efficient BDD Algorithms for FSM Synthesis and Verification.
Tuning sat checkers for bounded model-checking
Search Algorithms for Satisfiability Problems in Combinational Switching Circuits.
Algorithms for Solving Boolean Satisfiability in Combinational Circuits.

Combinational Test Generation Using Satisfiability.
Combining decision diagrams and sat procedures for efficient symbolic model checking.
A Decision Procedure for Propositional Logic.
SATO: An Efficient Propositional Prover.
--TR
Automatic verification of finite-state concurrent systems using temporal logic specifications
Graph-based algorithms for Boolean function manipulation
A structure-preserving clause form translation
Representing circuits more efficiently in symbolic model checking
Model checking and abstraction
Symbolic model checking
Model checking and modular verification
Model checking and abstraction
Computer-aided verification of coordinating processes
An intermediate design language and its analysis
Algorithms for solving Boolean satisfiability in combinational circuits
Symbolic model checking using SAT procedures instead of BDDs
A Computing Procedure for Quantification Theory
Symbolic Model Checking
Symbolic Model Checking without BDDs
Symbolic Reachability Analysis Based on SAT-Solvers
The Industrial Success of Verification Tools Based on StMYAMPERSANDaring;lmarck''s Method
Design Constraints in Symbolic Model Checking
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
Tuning SAT Checkers for Bounded Model Checking
Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams
Analyzing a PowerPCTM620 Microprocessor Silicon Failure Using Model Checking
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic
Verification of the Futurebus+ Cache Coherence Protocol
Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K
SATO

--CTR
Wojciech Penczek , Alessio Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae, v.55 n.2, p.167-185, May
M. Kacprzak , A. Lomuscio , W. Penczek, From Bounded to Unbounded Model Checking for Temporal Epistemic Logic, Fundamenta Informaticae, v.63 n.2-3, p.221-240, April 2004
Alex Aiken , Suhabe Bugrara , Isil Dillig , Thomas Dillig , Brian Hackett , Peter Hawkins, An overview of the saturn project, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.43-48, June 13-14, 2007, San Diego, California, USA
Stephanie Kemper , Andr Platzer, SAT-based Abstraction Refinement for Real-time Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 182, p.107-122, June, 2007
Wojciech Penczek , Alessio Lomuscio, Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking, Fundamenta Informaticae, v.55 n.2, p.167-185, April
Liang Zhang , Mukul R. Prasad , Michael S. Hsiao , Thomas Sidle, Dynamic abstraction using SAT-based BMC, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
W. Penczek , A. Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
Liang Zhang , M. R. Prasad , M. S. Hsiao, Incremental deductive & inductive reasoning for SAT-based bounded model checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.502-509, November 07-11, 2004
Clark Barrett , Leonardo Moura , Aaron Stump, Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006), Formal Methods in System Design, v.31 n.3, p.221-239, December  2007
Indradeep Ghosh , Mukul R. Prasad, A Technique for Estimating the Difficulty of a Formal Verification Problem, Proceedings of the 7th International Symposium on Quality Electronic Design, p.63-70, March 27-29, 2006
Matti Jrvisalo , Tommi Junttila , Ilkka Niemel, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Annals of Mathematics and Artificial Intelligence, v.44 n.4, p.373-399, August    2005
Dionisio de Niz , Peter H. Feiler, Aspects in the industry standard AADL, Proceedings of the 10th international workshop on Aspect-oriented modeling, p.15-20, March 12-12, 2007, Vancouver, Canada
Boena Wona, ACTLS properties and Bounded Model Checking, Fundamenta Informaticae, v.63 n.1, p.65-87, January 2004
Panagiotis Manolios , Sudarshan K. Srinivasan , Daron Vroon, Automatic memory reductions for RTL model verification, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
Nadia Creignou , Herv Daud , John Franco, A sharp threshold for the renameable-Horn and the q-Horn properties, Discrete Applied Mathematics, v.153 n.1, p.48-57, 1 December 2005
Harald Rue , Leonardo de Moura, Simulation and verification I: from simulation to verification (and back), Proceedings of the 35th conference on Winter simulation: driving innovation, December 07-10, 2003, New Orleans, Louisiana
K. Subramani , John Argentieri, Chain programming over difference constraints, Nordic Journal of Computing, v.13 n.4, p.309-327, December 2006
Carsten Sinz, Visualizing SAT Instances and Runs of the DPLL Algorithm, Journal of Automated Reasoning, v.39 n.2, p.219-243, August    2007
Schafer , Heike Wehrheim, The Challenges of Building Advanced Mechatronic Systems, 2007 Future of Software Engineering, p.72-84, May 23-25, 2007
Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February
Alur , Thao Dang , Franjo Ivani, Predicate abstraction for reachability analysis of hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.1, p.152-199, February 2006
Tobias Schuele , Klaus Schneider, Bounded model checking of infinite state systems, Formal Methods in System Design, v.30 n.1, p.51-81, February  2007
Henry Kautz , Bart Selman, The state of SAT, Discrete Applied Mathematics, v.155 n.12, p.1514-1524, June, 2007
Lucas Bordeaux , Youssef Hamadi , Lintao Zhang, Propositional Satisfiability and Constraint Programming: A comparative survey, ACM Computing Surveys (CSUR), v.38 n.4, p.12-es, 2006
model checking;cone of influence reduction;processor verification;bounded model checking;satisfiability