Abstract
A system of conservative transformation rules is presented for abstracting memories whose forwarding logic interacts with stalling conditions for preserving the memory semantics in microprocessors with in-order execution. Microprocessor correctness is expressed in the logic of Equality with Uninterpreted Functions and Memories (EUFM) [6]. Memory reads and writes are abstracted as arbitrary uninterpreted functions in such a way that the forwarding property of the memory semantics— that a read returns the data most recently written to an equal write address—is satisfied completely only when exactly the same pair of one read and one write address is compared for equality in the stalling logic. These transformations are applied entirely automatically by a tool for formal verification of microprocessors, based on EUFM, the Burch and Dill flushing technique [6], and the properties of Positive Equality [3]. An order of magnitude reduction is achieved in the number of e ij Boolean variables [9] that encode the equality comparisons of register identifiers in the correctness formulas for single-issue pipelined and dual-issue superscalar microprocessors with multicycle functional units, exceptions, and branch prediction. That results in up to 40× reduction in the CPU time for the formal verification of the dual-issue superscalar microprocessors.
This research was supported by the SRC under contract 00-DC-684.
Chapter PDF
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 Surveys, Vol. 24, No. 3 (September 1992), pp. 293–318.
R.E. Bryant, S. German, and M.N. Velev, “Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,”2 ACM Transactions on Computational Logic (TOCL), Vol. 2, No. 1 (January 2001).
R.E. Bryant, and M.N. Velev, “Boolean Satisfiability with Transitivity Constraints,”2 Computer-Aided Verification (CAV’ 00), E.A. Emerson and A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 86–98
R.E. Bryant, and M.N. Velev, “Boolean Satisfiability with Transitivity Constraints,”2 Technical Report CMU-CS-00-101, Carnegie Mellon University, 2000.
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. 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, 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.
J.L. Hennessy, and D.A. Patterson, Computer Architecture: A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, San Francisco, CA, 1996.
R. Hosabettu, “Systematic Verification of Pipelined Microprocessors,” Ph.D. thesis, Department of Computer Science, University of Utah, August 2000. http://www.cs.utah.edu/~hosabett.
S. Malik, A.R. Wang, R.K. Brayton, and A. Sangiovani-Vincentelli, “Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment,” International Conference on Computer-AIded Design (ICCAD’ 88), November 1988, pp. 6–9.
G. Ritter, H. Eveking, and H. Hinrichsen, “Formal Verification of Designs with Complex Control by Symbolic Simulation,” Correct Hardware Design and Verification Methods (CHARME’ 99), L. Pierre and T. Kropf, eds., LNCS 1703, Springer-Verlag, September 1999, pp. 234–249.
R. Rudell, “Dynamic Variable Ordering for Ordered Binary Decision Diagrams,” International Conference on Computer-Aided Design (ICCAD’93), November 1993, pp. 42–47.
M.N. Velev, and R.E. Bryant, “Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors,”2 36th Design Automation Conference (DAC’ 99), June 1999, pp. 397–401.
M.N. Velev, and R.E. Bryant, “Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic,”2 Correct Hardware Design and Verification Methods (CHARME’ 99), L. Pierre and T. Kropf, eds., LNCS 1703, Springer-Verlag, September 1999, pp. 37–53.
M.N. Velev, and R.E. Bryant, “Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction,”2 37th Design Automation Conference (DAC’ 00), June 2000, pp. 112–117.
M.N. Velev, and R.E. Bryant, “Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction,”2 Technical Report CMU-CS-00-116, Carnegie Mellon University, 2000.
M.N. Velev, “Formal Verification of VLIW Microprocessors with Speculative Execution,”2 Computer-Aided Verification (CAV’ 00), E.A. Emerson and A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 296–311.
M.N. Velev, and R.E. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,”2 submitted for publication, 2000.
M.N. Velev, and R.E. Bryant, “EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations,”2 submitted for publication, 2001.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Velev, M.N. (2001). Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_18
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive