loading...
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs
Charlotte, NC, USA September 30-October 02
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TEST.2003.1270834International Test Conference 2003 (I ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Miroslav N. Velev, "Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs," Test Conference, International, pp. 138, International Test Conference 2003 (ITC'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/TEST.2003.1270834,
author = {Miroslav N. Velev},
title = {Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs},
journal ={Test Conference, International},
volume = {0},
year = {2003},
issn = {1089-3539},
pages = {138},
doi = {http://doi.ieeecomputersociety.org/10.1109/TEST.2003.1270834},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Test Conference, International
TI - Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs
SN - 1089-3539
SP
EP
A1 - Miroslav N. Velev,
PY - 2003
KW - null
VL - 0
JA - Test Conference, International
ER -
 
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.