Advertisement

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

  • Miroslav N. Velev
  • Randal E. Bryant
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)

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.

References

  1. [1]
    W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954.Google Scholar
  2. [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. [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. [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. [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. [6]
    J.R. Burch, “Techniques for Verifying Superscalar Microprocessors,” 33rd Design Automation Conference (DAC’96), June 1996, pp. 552–557.Google Scholar
  7. [7]
  8. [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. [9]
  10. [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. [11]
    C.A.R. Hoare, “Proof of Correctness of Data Representations,” Acta Informatica, 1972, Vol. 1, pp. 271–281.zbMATHCrossRefGoogle Scholar
  12. [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. [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. [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. [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. [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. [17]
    Stanford Validity Checker (SVC), URL: http://sprout.Stanford.EDU/SVC.
  18. [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. [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. [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. [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. [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

Authors and Affiliations

  • Miroslav N. Velev
    • 1
  • Randal E. Bryant
    • 1
  1. 1.Department of Electrical and Computer Engineering School of Computer ScienceCarnegie Mellon UniversityUSA

Personalised recommendations