loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Miroslav N. Velev, Georgia Institute of Technology, Atlanta
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.