Efficient validity checking for processor verification
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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.Keywords
This publication has 10 references indexed in Scilit:
- Correctness verification of VLSI modules supported by a very efficient Boolean proverPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- The Stanford FLASH multiprocessorPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Applying formal verification to a commercial microprocessorPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal modeling and verification of microprocessorsIEEE Transactions on Computers, 1995
- Automatic verification of pipelined microprocessorsPublished by Association for Computing Machinery (ACM) ,1994
- Formal verification of a pipelined microprocessorIEEE Software, 1990
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- A Practical Decision Procedure for Arithmetic with Function SymbolsJournal of the ACM, 1979
- Efficiency of a Good But Not Linear Set Union AlgorithmJournal of the ACM, 1975