CMU-CS-98-131Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-98-131
Yirng-An Chen May 1998 Ph.D. Thesis
CMU-CS-98-131.ps
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
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. 130 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |