Collection of high-level microprocessor bugs from formal verification of pipelined and superscalar designs

被引：0
作者：
Velev, MN [1 ]
机构：
[1] Georgia Inst Technol, Sch Elect & Comp Engn, Atlanta, GA 30332 USA
来源：
INTERNATIONAL TEST CONFERENCE 2003, PROCEEDINGS | 2003年
关键词：
D O I：
暂无
中图分类号：
T [工业技术];
学科分类号：
08 ;
摘要：
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 microprocessor testing.
引用
收藏
页码：138 / 147
页数：10
相关论文
共 52 条
[1]  
Aagaard MD, 2002, LECT NOTES COMPUT SC, V2517, P123
[2]  
AAGAARD MD, 1995, INT C COMP AID DES N
[3]  
AAGAARD MD, 2002, IN PRESS SOFTWARE TO
[4]  
Albin K, 2001, DES AUT CON, P249, DOI 10.1109/DAC.2001.935513
[5]  
[Anonymous], LNCS
[6]  
Avizienis A., 1999, Dependable Computing for Critical Applications 7, P3, DOI 10.1109/DCFTS.1999.814287
[7]  
BEATTY DL, 1993, THESIS CARNEGIE MELL
[8]  
Bentley B, 2001, DES AUT CON, P244
[9]  
BENTLEY B, 2001, INTEL TECHNOLOGY J
[10]  
Bryant R.E, 2001, ACM Trans. Comput. Logic (TOCL), V2, P93
123456