Verification of pipelined microprocessors by comparing memory execution sequences in symbolic simulation
This paper extends Burch and Dill's pipeline verification method  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) , 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.
Keywordspipelined microprocessor verification memory shadowing Efficient Memory Model (EMM) circuit correspondence checking symbolic simulation
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- J. R. Burch, “Techniques for Verifying Superscalar Microprocessors,” DAC '96, June 1996, pp. 552–557.Google Scholar
- 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
- 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
- M. Pandey, “Formal Verification of Memory Arrays,” Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1997.Google Scholar
- 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
- 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
- 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
- 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