Abstract
We present a systematic approach to decompose and incrementally build the proof of correctness of pipelined microprocessors. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect (on the observables) of completing the instruction. In addition to avoiding term-size and case explosion problem that limits the pure flushing approach, our method helps localize errors, and also handles stages with iterative loops. The technique is illustrated on a pipelined and a superscalar pipelined implementations of a subset of the DLX architecture. It has also been applied to a processor with out-of-order execution.
This work was done in part when Ravi Hosabettu was visiting SRI International in summer 1997. The work done by the authors at University of Utah was supported in part by DARPA under Contract #DABT6396C0094 (Utah Verifier) and NSF MIP MIP-9321836. The work done by the authors at SRI International was supported in part under NASA Contract NASI-20334 and ARPA Contract A721/NAG 2-891.
Chapter PDF
Keywords
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
Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Srivas and Camilleri [14], pages 187–201.
J. R. Burch. Techniques for verifying superscalar microprocessors. In Design Automation Conference, DAC '96, June 1996.
J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In David Dill, editor, Computer-Aided Verification, CAV '91, volume 818 of Lecture Notes in Computer Science, pages 68–80, Stanford, CA, June 1994.Springer-Verlag.
D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design (TPCD '94), volume 910 of Lecture Notes in Computer Science, pages 203–222, Bad Herrenalb, Germany, September 1994. Springer-Verlag.
David Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993.
David Cyrluk. Inverting the abstraction mapping: A methodology for hardware verification. In Srivas and Camilleri [14], pages 172–186.
John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, 1990.
Ravi Hosabettu. PVS specification and proofs of the DLX, superscalar DLX examples and the processor with out-of-order execution, 1998. Available at http://www.cs.utah.edu/-hosabett/pvs/processor.html.
R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In International Conference on Computer Aided Design, ICCAD '95, 1995.
Jeremy Levitt and Kunle Olukotun. A scalable formal verification methodology for pipelined microprocessors. In Design Automation Conference, DAC '96, June 1996.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
Seungjoon Park and David L. Dill. Protocol verification by aggregation of distributed actions. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, pages 300–310, New Brunswick, NJ, July/August 1996. Springer-Verlag.
J. Sawada and W. A. Hunt, Jr. Trace table based approach for pipelined microprocessor verification. In Orna Grumberg, editor, Computer-Aided Verification, CAV '97, volume 1254 of Lecture Notes in Computer Science, pages 364–375, Haifa, Israel, June 1997. Springer-Verlag.
Mandayam Srivas and Albert Camilleri, editors. Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, November 1996. Springer-Verlag.
Mandayam K. Srivas and Steven P. Miller. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods in Systems Design, 8(2):153–188, March 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hosabettu, R., Srivas, M., Gopalakrishnan, G. (1998). Decomposing the proof of correctness of pipelined microprocessors. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028739
Download citation
DOI: https://doi.org/10.1007/BFb0028739
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive