Arithmetic Circuit Verification Based on Word-Level Decision Diagrams
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1998
- Accession Number
- ADA350486
Entities
People
- Yirng-an Chen
Organizations
- Carnegie Mellon University