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 repre-
sented 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 sequence
4
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
k = 0, 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 k = 0. This 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, s
0
, 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 SMV
1
version 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.
13