EECS 298-11: CAD Seminar
Wednesday, June 2, 10:30AM
531 Cory Hall, Hogan Room

                        Word Level Model Checking
       
                          Prof. Edmund M. Clarke
                        Carnegie Mellon University

Proving the correctness of arithmetic operations has always been an important
problem. The importance of this problem has been recently underscored by the
highly-publicized division error in the Pentium.  Although symbolic model
checking techniques based on Binary Decision Diagrams (BDDs) have been
successful in verifying control logic, these techniques cannot be used directly
for verifying arithmetic circuits.  In order to verify arithmetic circuits in
this manner, it is necessary to be able represent and manipulate functions that
map boolean vectors to integer values.

Bryant and Chen have developed a representation called the Binary Moment
Diagram (BMD).  They use the expansion $f = f|_{x=0} + x f'$, where $f'$ is
equal to $f|_{x=1} - f|_{x=0}$, instead of the Shannon expansion.  This gives a
compact representation for certain functions that have exponential size MTBDDs.
They have used this representation to verify the data paths of some arithmetic
circuits.  The BMD representation for both the circuit and the specification
are constructed and compared.  The circuit is correct if both BMDs are exactly
the same. However, depending on the implementation and the control logic, there
can be cases in which the circuit is correct but the BMDs are not identical.
Another problem is that this approach cannot handle inequalities.  Thus, it is
impossible to check some of the properties that are needed in order to avoid
the Pentium error.

We have combined both approaches.  We have used a hybrid representation for the
integer functions that occur in the arithmetic circuit verification. For the
state variables corresponding to data bits, this representation behaves like a
BMD, while for the state variables corresponding to control signals, it behaves
like a MTBDD.  By using this representation, we are able to handle circuits
with both control logic and wide data paths.

Furthermore, we have extended the symbolic model checking system SMV so that it
can also handle properties involving relationships among data words. In the
original SMV system, atomic formulas can only contain state variables.  In the
extended system, we allow atomic formulas to be equations or inequalities
between expressions as well.  These expressions are represented as hybrid BDDs.
We have developed efficient algorithms to compute the set of variable
assignments that would make these equations and inequalities true.  For the
class of linear functions, which includes many of the functions that occur in
practice, such operations are guaranteed to have complexity that is polynomial
in the width of the data words.

By using the extended model checking system, we have successfully verified
circuits for division and square root computation that are based on the SRT
algorithm used by the Pentium. We are able to handle both the control logic and
the data paths.  The total number of state variables exceeds 600 (which is much
larger than any circuit previously checked by SMV). We plan to apply the
technique to other arithmetic circuits in the near future.
    
(Joint work with Xudong Zhao.)