Paper Authors

Abstract

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract

Session 1532

Integrating Formal Verification into an Advanced Computer Architecture Course

Miroslav N. Velev mvelev@ece.gatech.edu School of Electrical and Computer Engineering Georgia Institute of Technology, Atlanta, GA 30332, U.S.A.

Abstract. The paper presents a sequence of three projects on design and formal verification of pipelined and superscalar processors. The projects were integrated—by means of lectures and pre- paratory homework exercises—into an existing advanced computer architecture course taught to both undergraduate and graduate students in a way that required them to have no prior knowledge of formal methods. The first project was on design and formal verification of a 5-stage pipelined DLX processor, implementing the six basic instruction types—register-register-ALU, register- immediate-ALU, store, load, jump, and branch. The second project was on extending the processor from project one with ALU exceptions, a return-from-exception instruction, and branch prediction; each of the resulting models was formally verified. The third project was on design and formal ver- ification of a dual-issue superscalar version of the DLX from project one. The preparatory home- work problems included an exercise on design and formal verification of a staggered ALU, pipelined in the style of the integer ALUs in the Intel Pentium 4. The processors were described in the high-level hardware description language AbsHDL that allows the students to ignore the bit widths of word-level values and the internal implementations of functional units and memories, while focusing entirely on the logic that controls the pipelined or superscalar execution. The formal verification tool flow included the term-level symbolic simulator TLSim, the decision procedure EVC, and an efficient SAT-checker; this tool flow—combined with the same abstraction techniques for defining processors with exceptions and branch prediction, as used in the projects—was applied at Motorola to formally verify a model of the M•CORE processor, and detected bugs. The course went through two iterations—offered at the Georgia Institute of Technology in the summer and fall of 2002—and was taught to 67 students, 25 of whom were undergraduates.

1. Introduction Verification is increasingly becoming the bottleneck in the design of state-of-the-art computer systems, with up to 70% of the engineering effort spent on verifying a new product1. The increased complexity of new microprocessors leads to more errors—Bentley2 reported a 350% increase in the number of bugs detected in the Intel Pentium 43, compared to those detected in the previous architecture, the Intel Pentium Pro4, 5. Formal verification—the mathematical proof of correctness of hardware and software—is gaining momentum in industrial use, but has so far failed to scale for realistic microprocessors, or has required extensive manual intervention by experts—factors that have made formal verification impractical to integrate in existing computer architecture courses.

Proceedings of the 2003 American Society for Engineering Education Annual Conference & Exposition Copyright © 2003, American Society for Engineering Education

• Citation

• Format
  • APA
  • APA - LaTeX bibitem
  • MLA
  • MLA - LaTeX bibitem
  • Bibtex
  • EndNote - RIS

Velev, M. (2003, June), Integrating Formal Verification Into An Advanced Computer Architecture Course Paper presented at 2003 Annual Conference, Nashville, Tennessee. 10.18260/1-2--11927