Yirng-An Chen

Arithmetic Circuit Verification Based on Word-Level Decision Diagrams Degree Type: Ph.D. in Computer Science
Advisor(s): Randal Bryant
Graduated: May 1998

Abstract:

The division bug in Intel's Pentium processor has demonstrated the importance and the difficulty of verifying arithmetic circuits and the high cost of an arithmetic bug. In this thesis, we develop verification methodologies and symbolic representations for functions mapping Boolean vectors to integer or floating-point values, and build verification systems for arithmetic circuits.

Our first approach is based on a hierarchical methodology and uses multiplicative binary moment diagrams (*BMDs) to represent functions symbolically for verification of integer circuits. *BMDs are particularly effective for representing and manipulating functions mapping Boolean vectors to integer values. Our hierarchical methodology exploits the modular structure of arithmetic circuits to speed up the verification task. Based on this approach, we have verified a wide range of integer circuits such as multipliers and dividers.

Our *BMD-based approach cannot be directly applied to verify floating-point (FP) circuits. The first challenge is that the existing word-level decision diagrams cannot represent floating-point functions efficiently. For this problem, we introduce Multiplicative Power Hybrid Decision Diagrams (*PHDDs) to represent floating-point functions efficiently. *PHDDs explode during the composition of specifications in the rounding module in the hierarchical approach. To overcome this problem, we choose to verify flattened floating-point circuits by using word-level SMV with these improvements: *PHDDs, conditional symbolic simulation and a short-circuiting technique.

Using extended word-level SMV, FP circuits are treated as black boxes and verified against reusable specifications. The FP adder in the Aurora III Chip at the University of Michigan was verified. Our system found several errors in the design and generated a counterexample for each error. A variant of the corrected FP adder was created and verified to illustrate the ability of our system to handle different designs. For each FP adder, verification took 2 CPU hours. We believe that our system and specifications can be applied to directly verify other FP adder designs and to help find design errors. We believe that our system can be used to verify the correctness of conversion circuits which translate data from one format to another.

Thesis Committee:
Randal E. Bryant (Chair)
Edmund M. Clarke
Rob. A. Rutenbar
Xudong Zhao (Intel Corporation)

James Morris, Head, Computer Science Department
Raj Reddy Dean, School of Computer Science

Keywords:
Binary moment diagram, *BMD, hybrid decision diagram, HDD, K*BMD, multiplicative power hybrid decision diagram, *PHDD, arithmetic circuit, floating-point adder, IEEE standard, formal verification, theorem proving, binary decision diagram, MTBDD, EVBDD, FDD, KFDD, K*BMD, model checking, SMV