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.
Acknowledgements
We would like to thank Amit Goel for implementing a translation procedure from propositional logic to CNF, the input format of SATO and GRASP. We express our gratitude to Steven German of IBM for his detailed comments on this paper. We also extend our thanks to João Marques-Silva of the Technical University in Lisbon, Portugal, for his help with GRASP, to Clark Barrett of Stanford University for his help with SVC, to G. Stålmarck of Prover Technology AB, Sweden (URL: http:// www.prover.com), for licensing a copy of Prover to Carnegie Mellon University, and to Arne Borälv of the same company for helping us use Prover efficiently.
Chapter PDF
Similar content being viewed by others
Keywords
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
W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954.
R.E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Serveys, Vol. 24, No. 3 (September 1992), pp. 293–318.
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.
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.
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.
J.R. Burch, “Techniques for Verifying Superscalar Microprocessors,” 33rd Design Automation Conference (DAC’96), June 1996, pp. 552–557.
CUDD-2.3.0,URL: http://vlsi.colorado.edu/~fabio.
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.
GRASP,URL: http://andante.eecs.umich.edu.
J.L. Hennessy, and D.A. Patterson, Computer Architecture: A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, San Francisco, CA, 1996.
C.A.R. Hoare, “Proof of Correctness of Data Representations,” Acta Informatica, 1972, Vol. 1, pp. 271–281.
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.
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.
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.
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.
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.
Stanford Validity Checker (SVC), URL: http://sprout.Stanford.EDU/SVC.
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.
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.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Velev, M.N., Bryant, R.E. (1997). Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_5
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive