Reference:

Robert B. Jones, David L. Dill, and Jerry R. Burch. Efficient validity checking for processor verification. In International Conference on Computer-Aided Design (ICCAD), pages 2-6. IEEE Computer Society Press, November 1995.

Abstract:

We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessor control circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@InProceedings{JonesDillBurch95ICCAD,
  author    = {Robert B. Jones and 
               David L. Dill and 
               Jerry R. Burch},
  title     = {Efficient Validity Checking for Processor Verification},
  pages     = {2--6},
  booktitle = {International Conference on Computer-Aided Design (ICCAD)},
  publisher = {IEEE Computer Society Press},
  month     = {November},
  year      = 1995,
}