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.
Citation:
Miroslav N. Velev, "Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs," itc, pp.138, International Test Conference 2003 (ITC'03), 2003 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||