Abstract
We present a way to abstract functional units in symbolic simulation of actual circuits, thus achieving the effect of uninterpreted functions at the bit-level. Additionally, we propose an efficient encoding technique that can be used to represent uninterpreted symbols with BDDs, while allowing these symbols to be propagated by simulation with a conventional bit-level symbolic simulator. Our abstraction and encoding techniques result in an automatic symmetry reduction and allow the control and forwarding logic of the actual circuit to be used unmodified. The abstraction method builds on the behavioral Efficient Memory Model [18][19] and its capability to dynamically introduce consistent initial state, which is identical for two simulation sequences. We apply the abstraction and encoding ideas on the verification of pipelined microprocessors by correspondence checking, where a pipelined microprocessor is compared against a non-pipelined specification.
This research was supported in part by the SRC under contract 98-DC-068.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Berezin, A. Biere, E. M. Clarke, and Y. Zhu, “Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification,” FMCAD’98 (appears in this publication).
S. Bose, and A.L. Fisher, “Verifying Pipelined Hardware Using Symbolic Logic Simulation,” International Conference on Computer Design, October 1989, pp. 217–221.
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, and M. N. Velev, “Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation,” Asian Computer Science Conference (ASIAN’97), R.K. Shyamasundar and K. Ueda, eds., LNCS 1345, Springer-Verlag, December 1997, pp. 18–31.
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.
J. R. Burch, “Techniques for Verifying Superscalar Microprocessors,” DAC’96, June 1996, pp. 552–557.
Y.-A. Chen, “Arithmetic Circuit Verification Based on Word-Level Decision Diagrams,” Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1998.
A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal, “BDD Based Procedures for a Theory of Equality with Uninterpreted Functions,” CAV’98, June, 1998.
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. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation,” Ph.D. thesis, Department of Electrical and Computer Engineering, Carnegie Mellon University, August 1997.
T.-H. Liu, K. Sajid, A. Aziz, and V. Singhal, “Optimizing Designs Containing Black Boxes,” 34th Design Automation Conference, June 1997, pp. 113–116.
G. Nelson, and D.C. Oppen, “Simplification by Cooperating Decision Procedures,” ACM Transactions on Programming Languages and Systems, Vol. 1, No. 2, October 1979, pp. 245–257.
M. Pandey, “Formal Verification of Memory Arrays,” Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1997.
D.A. Patterson, and J.L. Hennessy, Computer Organization and Design: The Hardware/Software Interface, 2nd Edition, Morgan Kaufmann Publishers, San Francisco, CA, 1998.
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.
R.E. Shostak, “A Practical Decision Procedure for Arithmetic with Function Symbols,” J. ACM, Vol. 26, No. 2, April 1979, pp. 351–360.
M.N. 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.
M.N. Velev, and R.E. Bryant, “Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation,” International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), B. Steffen, ed., LNCS 1384, Springer-Verlag, March-April 1998, pp. 136–150.
M.N. Velev, and R.E. Bryant, “Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation,” International Conference on Application of Concurrency to System Design (CSD’98), IEEE Computer Society, March 1998, pp. 200–212.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Velev, M.N., Bryant, R.E. (1998). Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_3
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive