International Test Conference 2003 (ITC'03)
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs
Charlotte, NC, USA
September 30-October 02
ISBN: 0-7803-8107-6
The paper presents a collection of 93 different bugs, detected in formal verification of 65 student designs that include: 1) single-issue pipelined DLX processors; 2) extensions with exceptions and branch prediction; and 3) dual-issue superscalar implementations. The processors were described in a high-level HDL, and were formally verified with an automatic tool flow. The bugs are analyzed and classified, and can be used in research on micro-processor testing.