Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic
We present a collection of ideas that allows the pipeline verification method pioneered by Burch and Dill  to scale very efficiently to dual-issue super- scalar processors. We achieve a significant speedup in the verification of such processors, compared to the result by Burch , while using an entirely automatic tool. Instrumental to our success are exploiting the properties of positive equality  and the simplification capabilities of BDDs.
KeywordsPositive Equality Function Symbol Domain Variable Propositional Formula Correctness Criterion
- W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954.Google Scholar
- R.E. Bryant, S. German, and M.N. Velev, “Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions, “2 Computer-Aided Verification (CAV’99), LNCS, Springer-Verlag, June 1999.Google Scholar
- R.E. Bryant, S. German, and M.N. Velev, “Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,”2 Technical Report CMU-CS-99-115, Carnegie Mellon University, 1999.Google Scholar
- J.R. Burch, “Techniques for Verifying Superscalar Microprocessors,” 33rd Design Automation Conference (DAC’96), June 1996, pp. 552–557.Google Scholar
- CUDD-2.3.0,URL: http://vlsi.colorado.edu/~fabio.
- GRASP,URL: http://andante.eecs.umich.edu.
- R. Hojati, A. Kuehlmann, S. German, and R.K. Brayton, “Validity Checking in the Theory of Equality with Uninterpreted Functions Using Finite Instantiations,“ International Workshop on Logic Synthesis, May 1997.Google Scholar
- A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel, “Deciding Equality Formulas by Small-Domain Instantiations”, Computer-Aided Verification (CAV’99), LNCS, Springer-Verlag, June 1999.Google Scholar
- G. Stålmarck, “A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula”, Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995), 1989.Google Scholar
- Stanford Validity Checker (SVC), URL: http://sprout.Stanford.EDU/SVC.
- [18.M.N. Velev, and R.E. Bryant, “Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation,”2 International Conference on Application of Concurrency to System Design (CSD‘98), IEEE Computer Society, March 1998, pp. 200–212.Google Scholar
- M.N. Velev, and R.E. Bryant, “Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors,”2 36th Design Automaation Conference (DAC’99), June 1999, pp. 397–401.Google Scholar
- H. Zhang, “SATO: An Efficient Propositional Prover,” International Conference on Automated Deduction (CADE’97), LNAI 1249, Springer-Verlag, 1997, pp. 272–275. Available from: http://www.cs.uiowa.edu/~hzhang/sato.html.