Integrating formal verification into an advanced computer architecture course

This paper presents a sequence of three projects on design and formal verification of pipelined and superscalar processors: 1) a single-issue, five-stage DLX (an academic processor used widely for teaching pipelined execution and defined by Hennessy and Patterson in the first edition of their graduate textbook); 2) an extension of the DLX with exceptions and branch prediction; and 3) a dual-issue superscalar DLX. The projects were integrated into two editions of an advanced computer architecture course that was offered at the Georgia Institute of Technology, Atlanta, in the summer and fall 2002 and was taught to 67 students (25 of whom were undergraduates) in a way that required them to have no prior knowledge of formal methods. Preparatory homework problems included an exercise on design and formal verification of a staggered Arithmetic Logic Unit (ALU), pipelined in the style of the integer ALUs in the Intel Pentium 4. The processors were designed and formally verified with a tool flow that was used to formally verify the M·CORE processor at Motorola and detected bugs.