Abstract
We describe a method for rigorously specifying and verifying the control of pipelined microprocessors which can be used by the hardware designer for a precise documentation and justification of the correctness of his design techniques. We proceed by successively refining a one-instruction-at-a-time-view of a RISC processor to a description of its pipelined implementation; the structure of the refinement hierarchy is determined by standard instruction pipelining principles (grouped following the kind of conflict they are designed to avoid: structural hazards, data hazards and control hazards).
We illustrate our approach through a formal specification with correctness proof of Hennessy and Patterson's RISC processor DLX but the method can be extended to complex commercial microprocessor design where traditional or purely automatic methods do not scale up. The specification method supports incremental design techniques; the modular proof method offers reusing proofs and supports the designer's intuitive reasoning, in particular “local” argumentations typical for upgrading and optimizing machines. Since our models come in the form of Abstract State Machines, they can be made executable by ASM interpreters and can thereby be used for prototypical simulations.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M.Aagaard and M.Leeser. Reasoning About Pipelines with Structural Hazards, Springer LNCS 901, 1995.
W. Ahrendt. Von PROLOG zur WAM, Verifikation der Prozedurübersetzung mit KIV. Diploma thesis, University of Karlsruhe, December 1995, pp.115.
T.Arora, T.Leung, K.Levitt, T.Schubert, and P.Windley: Report on the UCD microcoded Viper verification project. Springer LNCS 780, 1994, 239–252.
D.L.Beatty. A Methodology for Formal Hardware Verification, with Application to Microprocessors. PhD thesis, School of CS, CMU, Aug. 1993.
E. Börger. Why use evolving algebras for hardware and software engineering. in: M. Bartosek, J. Staudek, J. Wiedermann (Eds), SOFSEM'95, Springer LNCS 1012, 1995, 236–271.
E. Börger and G. Del Castillo. A formal method for provably correct composition of a real-life processor out of basic components (The APE100 reverse engineering project). In: Proc. First IEEE International Conference Engineering of Complex Computer Systems (ICECCS'96). IEEE Comp. Soc. Press, Los Alamitos CA, 1995, 145–148.
E. Börger and I. Durdanović. Correctness of Compiling Occam to Transputer Code. in: Computer Journal 39, 1996, 52–92.
E. Börger and S. Mazzzanti. A Correctness Proof for Pipelinening in RISC Architectures DIMACS Technical Report 96-22, July 1996, pp.60.
E. Börger and D. Rosenzweig. The WAM — Definition and Compiler Correctness. in: Logic Programming: Formal Methods and Practical Applications (C.Beierle, L.Plümer, Eds.), Elsevier Science, 1995, 20–90 (chapter 2).
J.P.Bowen. Formal specifacation and documentation of microprocessor instruction sets. In: Microprocessing and Microprogramming 21, 223–230, 1987.
O. Buckow and J. Bormann. Formale Spezifikation und Verifikation eines SPARC-kompatiblen Prozessors mit einem interaktiven Beweissystem, Siemens Research and Development, München 1993.
J.R. Burch and D.L.Dill. Automatic verification of pipelined microprocessor control. Conf. on Computer-Aided Verification, 1994.
J.A. Cohn. A proof of correctness of the VIPER microprocessor: The first level. In G.Birtwhistle and P.Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 27–72. Kluwer Academic Publisher, 1988.
J.A. Cohn. Correctness properties of the Viper block model: The second level. In: G.Birtwistle, editor, Proceedings of the 1988 Design Verification Conference. Springer-Verlag, 1989.
D.Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI CS Lab, 1993.
D.Cyrluk. A PVS specification, implementation and verification of DLX. SRI, Palo Alto (Oral Communication).
M. Dehof. Formale Spezifikation und Verifikation des DLX-RISC-Prozessors. Diploma Thesis, Inst. f. Technik der Informationsverarbeitung, University of Karlsruhe, August 1994.
M. Dehof and S. Tahar. Implementierung des DLX-RISC-Prozessors in einer Standardezellen-Entwurfsumgebung, Technical Report No. SBF 358-C2-9/94, Institute of Computer Design and Fault Tolerance, University of Karlsruhe, Germany, March 1994.
Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In: Specification and validation methods, Ed. E. Börger, Oxford University Press, 1995.
E. Harcourt, J.Mauney, and T.Cook. From processor timing specifications to static instruction scheduling. In Static Analysis Symposium, September 1994.
J.L. Hennessy. Designing a computer as a microprocessor: Experience and lessons from the MIPS 4000. A lecture at the Symposium on Integrated Systems, Seattle, Washington, March, 1993.
J.L. Hennessy and D.A. Patterson. Computer Architecture: a Quantitative Approach Morgan Kaufman Publisher, 1990. Revised second edition 1996.
J. Herbert. Incremental design and formal verification of microcoded microprocessor. In V. Stavridou, T.F. Melham, and R.T. Boute, editors, Theorem Provers in Cicruit Design, Proocedings of the IFIP WG 10.2 International Working Conference, Nijmegen, The Netherlands. North-Holland, June 1992.
J.Huggins. Kermit: specification and verification. In: Specification and validation methods, Ed. E. Börger, Oxford University Press, 1995.
W.A. Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5:429–460, 1989.
J.Joyce. Formal verification and implementation of a microprocessor. In: G.Birtwhistle and P.A.Subrahmanyan (Eds), VLSI specification, verification, and synthesis. Kluwer Ac. Press 1988.
J.Joyce. Multi-level verification of microprocessor-based systems. PhD thesis, Cambridge Dec. 89.
J.Joyce, G.Birtwistle, and M.Gordon. Proving a computer correct in higher order logic. TR 100, Computer Lab., University of Cambridge, 1986.
L.Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. on Computers, 1979, C-28, 690–691.
M.Langevin and E.Cerny. Verification of processor-like circuits. In: P.Prinetto and P.Camurati (Eds), Advanced research Workshop on Correct Hardware Dwsign Methodologies, June 1991.
C.Pusch. Verification of Compiler Correctness for the WAM. In: Proc. Theorem Proving in Higher Order Logics (TPHOL'97, Turku), Springer LNCS 1125, 1996.
A.W.Roscoe. Occam in the specification and verification of microprocessors. Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering, 339(1652): 137–151, Apr.15, 1992.
J.B.Saxe, S.J.Garland, J.V.Guttag and J.J.Horning. Using transformations and verification in circuit design. TR 78, DEC System Res. Center, 1991.
M. Srivas and M. Bickford. Formal verification af a pipelined microprocessor. IEEE Software, 7(5):52–64, September 1990.
S.Tahar. Eine Methode zur formalen Verifikation von RISC-Prozessoren. Fortschrittberichte VDI, Reihe 10: Informatik/Kommunikationstechnik Nr. 350, VDI-Verlag, Düsseldorf 1995, pp.XIV+162.
S.Tahar and R.Kumar. Towards a methodology for the formal hierarchical verification of RISC processors. Proc. IEEE Int.Conf. on Computer Design (ICCD93), Cambridge/Mass; Oct.1993, pp. 58–62.
S.Tahar and R.Kumar. Implementational issues for verifying RISC-pipeline conflicts in HOL. Springer LNCS 859, 1994, pp. 424–439.
S. Tahar and R.Kumar. A practical methodology for the formal verification of RISC processors. FZI TR Sept. 95, Karlsruhe, pp. iii+46.
P.J.Windley. A hierarchical methodology for verifying microprogrammed mircoprocessors. Proc. IEEE Symp. on Security and Privacy, Oakland, May 1990, pp. 345–357.
P.J. Windley. Formal modelling and verification of microprocessors. IEEE Transactions on Computers, 1994.
P.J. Windley. Specifying instruction-set architecture in HOL: a primer. Springer LNCS 859, 1994, pp. 440–455.
P.J. Windley and M.L. Coe. A Correctness Model for Pipelined Microprocessors. Springer LNCS 901.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Börger, E., Mazzanti, S. (1997). A practical method for rigorously controllable hardware design. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027289
Download citation
DOI: https://doi.org/10.1007/BFb0027289
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive