Accession Number : ADA296460

Title :   Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Clarke, E. ; Zhao, X.

PDF Url : ADA296460

Report Date : MAY 1995

Pagination or Media Count : 22

Abstract : The highly-publicized division error in the Pentium has emphasized the importance of formal verification of arithmetic operations. Symbolic model checking techniques based on binary decision diagrams (BDDs) have been successful in verifying control logic. However, lack of proper representation for functions that map boolean vectors into integers has prevented this technique from being used for verifying arithmetic circuits. We have used hybrid decision diagrams to represent the integer functions that occur in the arithmetic circuit verification. For the state variables corresponding to data bits, our representation behaves like a binary moment diagram (BMD) while for the state variables corresponding to control signals, it behaves like a multi-terminal BDD (MTBDD). By using this representation, we are able to handle circuits with both control logic and wide data paths. 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 could 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 decision diagrams. The extended model checking system enables us to verify 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). (kar) p. 3

Descriptors :   *ALGORITHMS, *SYSTEMS APPROACH, *CIRCUIT TESTERS, COMPUTATIONS, DECISION MAKING, DATA MANAGEMENT, DATA TRANSMISSION SYSTEMS, VERIFICATION, PATHS, VARIABLES, SIGNALS, WORDS(LANGUAGE), HYBRID SYSTEMS, EQUATIONS, ARITHMETIC, DIAGRAMS, SQUARE ROOTS, CONTROL SEQUENCES.

Subject Categories : Electrical and Electronic Equipment
      Numerical Mathematics

Distribution Statement : APPROVED FOR PUBLIC RELEASE