Bit-Level Analysis of an SRT Divider Circuit.

Abstract

It is impractical to verify multiplier or divider circuits entirely at the bit-level using ordered Binary Decision Diagrams (BDDs), because the BDD representations for these functions grow exponentially with the word size. It is possible, however, to analyze individual stages of these circuits using BDDs. Such analysis can be helpful when implementing complex arithmetic algorithms. As a demonstration, we show that Intel could have used BDDs to detect erroneous table entries in the Pentium floating point divider. Going beyond verification, we show that bit-level analysis can be used to generate a correct version of the table.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 18, 1995
Accession Number
ADA294842

Entities

People

  • Randal Bryant

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Circuit Analysis
  • Circuits
  • Computations
  • Computer Science
  • Demographic Cohorts
  • Diagrams
  • Floating Point Operations
  • Iterations
  • Logic
  • Logic Gates
  • Networks
  • Simulations
  • Specifications
  • Verification

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computer Programming and Software Development.