Verification of pipelined microprocessors by comparing memory execution sequences in symbolic simulation

  • Randal E. Bryant
  • Miroslav N. Velev
Invited Lecturers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


This paper extends Burch and Dill's pipeline verification method [4] to the bit level. We introduce the idea of memory shadowing, a new technique for providing on-the-fly identical initial memory state to two different memory execution sequences. We also present an algorithm which compares the final states of two memories for equality. Memory shadowing and the comparison algorithm build on the Efficient Memory Model (EMM) [13], a behavioral memory model where the number of symbolic variables used to characterize the initial state of a memory is proportional to the number of distinct symbolic locations accessed. These techniques allow us to verify that a pipelined circuit has equivalent behavior to its unpipelined specification by simulating two memory execution sequences and comparing their final states. Experimental results show the potential of the new ideas.


pipelined microprocessor verification memory shadowing Efficient Memory Model (EMM) circuit correspondence checking symbolic simulation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    S. Bose, and A. L. Fisher, “Verifying Pipelined Hardware Using Symbolic Logic Simulation,” International Conference on Computer Design, October 1989, pp. 217–221.Google Scholar
  2. [2]
    R. E. Bryant, “Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis,” International Conference on Computer Aided Design, November 1991, pp. 350–353.Google Scholar
  3. [3]
    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
  4. [4]
    J. R. Burch, and D. L. Dill, “Automated Verification of Pipelined Microprocessor Control,” CAV '94, D. L. Dill, ed., LNCS 818, Springer-Verlag, June 1994, pp. 68–80.Google Scholar
  5. [5]
    J. R. Burch, “Techniques for Verifying Superscalar Microprocessors,” DAC '96, June 1996, pp. 552–557.Google Scholar
  6. [6]
    C. A. R. Hoare, “Proof of Correctness of Data Representations,” Acta Informatica, 1972, Vol. 1, pp. 271–281.CrossRefGoogle Scholar
  7. [7]
    A. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation,” Ph.D. thesis, Department of Electrical and Computer Engineering, Carnegie Mellon University, August 1997.Google Scholar
  8. [8]
    R. B. Jones, C.-J. H. Seger, and D. L. Dill, “Self-Consistency Checking,” FMCAD '96, M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November 1996, pp. 159–171.Google Scholar
  9. [9]
    M. Pandey, “Formal Verification of Memory Arrays,” Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1997.Google Scholar
  10. [10]
    M. Pandey, and R. E. Bryant, “Exploiting Symmetry When Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation,” CAV '97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, pp. 244–255.Google Scholar
  11. [11]
    J. Sawada, and W. A. Hunt, Jr., “Trace Table Based Approach for Pipelined Microprocessor Verification,” CAV '97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, pp. 364–375.Google Scholar
  12. [12]
    C.-J. H. Seger, and R. E. Bryant, “Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories,” Formal Methods in System Design, Vol. 6, No. 2 (March 1995), pp. 147–190.CrossRefGoogle Scholar
  13. [13]
    M. Velev, R. E. Bryant, and A. Jain, “Efficient Modeling of Memory Arrays in Symbolic Simulation,” CAV '97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, pp. 388–399.Google Scholar
  14. [14]
    P. J. Windley, and J. R. Burch, “Mechanically Checking a Lemma Used in an Automatic Verification Tool,” FMCAD '96, M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November 1996, pp. 362–376.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Randal E. Bryant
    • 1
  • Miroslav N. Velev
    • 2
  1. 1.School of Computer ScienceUSA
  2. 2.Department of Electrical and Computer EngineeringCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations