@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(Verification of Arithmetic Circuits)
@heading(CMU-CS-96-149)
@center(@b(Xudong Zhao))
@center(August 1996 - Ph.D. Thesis)
@center(FTP: Unavailable)
@blankspace(1)
@begin(text,spacing=1)

The recent highly-publicized division error in the Pentium Processor 
has emphasized the importance of verification of arithmetic circuits.
Current dubugging techniques like simulation have difficulties in finding
such errors because the error occurrences can be every rare. We have
applied two different types of formal verification techniques to the problem.
One approach uses @i(word level model checking), and the other approach 
uses @i(theorem proving). 

Symbolic model checking techniques based on application of BDDs
have been widely used in verification of computer hardware systems.
However, lack of proper representation for integer valued functions has
prevented these methods from being used in verification of arithmetic 
circuits. In this thesis, we introduce a new representation, @i(hybrid
decision diagrams). This representation enables us to handle cicuits that
contain both control logic and wide data paths. By using hybrid decision
diagrams, we have extended the temporal logic and the symbolic model
checking algorithm. The extended algorithm, which we call word level
model checking, can be used to verify a large class of arithmetic circuits.

We have also investigated the possibility of verifying arithmetic
circuits using automatic theorem provers. We have built a theorem prover
called @i(Analytica) on top of the symbolic computation system @i(Mathematica).
Analytica is able to exploit the mathematical knowledge that is built
into the symbolic computation system. Such knowledge is very useful
in handling the complicated equations and inequalities which arise from 
verification of arithmetic circuits.

As an example, we have checked the correctness of a division circuit
that uses a radix-4 SRT division algorithm. The algorithm is simailar
to the one used in the Pentium. We have applied both verification
techniques on this circuit. In the word level model checking approach, a 
gate level model for the circuit is built. The specification is expressed by
formulas of the extended temporal logic. The word level model checking
system is able to decide that the model satisfies the specification. In the
theorem proving approach, the circuit is modeled in an abstract manner
where each component is described as one ore more axioms. The theorems
corresponding to the specification of the circuit is proved by Analytica
using the axioms as given facts.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Formal verification, arithmetic circuits, temporal logic,
CTL, word level CTL, symbolic model checking, word level model checking,
theorem proving, binary decision diagrams, multi-terminal binary
decision diagrams, binary moment diagrams, hybrid decision diagrams,
SRT division algorithm>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(189 pages)])