Abstract
Correspondence checking formally verifies that a pipelined microprocessor realizes the serial semantics of the instruction set model. By representing the circuit state symbolically with Ordered Binary Decision Diagrams (OBDDs), this correspondence checking can be performed directly on a logic-level representation of the circuit. Our ongoing research seeks to make his approach practical for real-life microprocessors.
This research was supported in part by the Defense Advanced Research Project Agency, Contract DABT63-96-C-0071, and in part by the Semiconductor Research Corporation, Contract 97-DC-068.
Chapter PDF
Keywords
- Formal Verification
- Instruction Sequence
- Abstraction Function
- Order Binary Decision Diagram
- Pipeline Structure
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
S. Bose, and A. L. Fisher, “Verifying Pipelined Hardware Using Symbolic Logic Simulation,” International Conference on Computer Design (ICCD '89), 1989, pp. 217–221.
R. E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams,” ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293–318.
J. R. Burch, and D. L. Dill, “Automated Verification of Pipelined Microprocessor Control,” Computer-Aided Verification (CAV'94), LNCS 818, Springer-Verlag, June, 1994, pp. 68–80.
C. A. R. Hoare, “Proof of Correctness of Data Representations,” Acta Informatica Vol. 1, 1972, pp. 271–281.
M. Kantrowitz, and L. M. Noack, “I'm Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha Microprocessor,” 33rd Design Automation Conference (DAC '96), 1996, pp. 325–330.
K. L. Nelson, A. Jain, and R. E. Bryant, “Formal Verification of a Superscalar Execution Unit,” 34th Design Automation Conference (DAC '97), June, 1997.
M. N. Velev, and R. E. Bryant, “Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation,” Asian Computer Science Conference (ASIAN '97), LNCS 1345, Springer-Verlag, December 1997, pp. 18–31.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bryant, R.E. (1998). Formal verification of pipelined processors. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054160
Download citation
DOI: https://doi.org/10.1007/BFb0054160
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive