# Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic

Conference paper

First Online:

## Abstract

We present a collection of ideas that allows the pipeline verification method pioneered by Burch and Dill [5] 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 [6], while using an entirely automatic tool. Instrumental to our success are exploiting the properties of positive equality [3][4] and the simplification capabilities of BDDs.

## Keywords

Positive Equality Function Symbol Domain Variable Propositional Formula Correctness Criterion
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Download
to read the full conference paper text

## References

- [1]W. Ackermann,
*Solvable Cases of the Decision Problem*, North-Holland, Amsterdam, 1954.Google Scholar - [2]R.E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Serveys, Vol. 24, No. 3 (September 1992), pp. 293–318.CrossRefGoogle Scholar
- [3]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 - [4]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 - [5]J.R. Burch, and D.L. Dill, “Automated Verification of Pipelined Microprocessor Control,”
*Computer-Aided Verification (CAV‘94)*, D.L. Dill, ed., LNCS 818, Springer-Verlag, June 1994, pp. 68–80. Available from: http://sprout.stanford.edu/papers.html.Google Scholar - [6]J.R. Burch, “Techniques for Verifying Superscalar Microprocessors,”
*33rd Design Automation Conference (DAC’96)*, June 1996, pp. 552–557.Google Scholar - [7]CUDD-2.3.0,URL: http://vlsi.colorado.edu/~fabio.
- [8]A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal, “BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, ”
*Computer-Aided Verification (CAV’98)*, A.J. Hu and M.Y. Vardi, eds., LNCS 1427, Springer-Verlag, June 1998, pp. 244–255.CrossRefGoogle Scholar - [9]GRASP,URL: http://andante.eecs.umich.edu.
- [10]J.L. Hennessy, and D.A. Patterson,
*Computer Architecture: A Quantitative Approach*, 2nd edition, Morgan Kaufmann Publishers, San Francisco, CA, 1996.zbMATHGoogle Scholar - [11]C.A.R. Hoare, “Proof of Correctness of Data Representations,”
*Acta Informatica*, 1972, Vol. 1, pp. 271–281.zbMATHCrossRefGoogle Scholar - [12]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 - [13]A.J. Isles, R. Hojati, and R.K. Brayton, “Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory, ”
*Computer-Aided Verification (CAV‘98)*, A.J. Hu and M.Y. Vardi, eds., LNCS 1427, Springer-Verlag, June 1998, pp. 256–267.CrossRefGoogle Scholar - [14]J.P. Marques-Silva, and K.A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability, ”
*IEEE Transactions on Computers*, Vol. 48, No. 5, May 1999, pp. 506–521.CrossRefMathSciNetGoogle Scholar - [15]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 - [16]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
- [17]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 - [19]M.N. Velev, and R.E. Bryant, “Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking,”
^{2}*Formal Methods in Computer-Aided Design (FMCAD’98)*, G. Gopalakrishnan and P. Windley, eds., LNCS 1522, Springer-Verlag, November 1998, pp. 18–35.CrossRefGoogle Scholar - [20]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 - [21]P.J. Windley, and J.R. Burch, “Mechanically Checking a Lemma Used in an Automatic Verification Tool, ”
*Formal Methods in Computer-Aided Design (FMCAD’96)*, M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November 1996, pp. 362–376.CrossRefGoogle Scholar - [22]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.

## Copyright information

© Springer-Verlag Berlin Heidelberg 1997