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
相关论文
共 50 条
  • [1] FORMAL VERIFICATION OF A PIPELINED MICROPROCESSOR
    SRIVAS, M
    BICKFORD, M
    IEEE SOFTWARE, 1990, 7 (05) : 52 - 64
  • [2] Formal Verification of High-Level Synthesis
    Herklotz, Yann
    Pollard, James D.
    Ramanathan, Nadesh
    Wickerson, John
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5 (OOPSLA):
  • [3] Formal Deadlock Checking on High-Level SystemC Designs
    Chou, Chun-Nan
    Hsu, Chang-Hong
    Chao, Yueh-Tung
    Huang, Chung-Yang
    2010 IEEE AND ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2010, : 794 - 799
  • [4] A formal verification method of scheduling in high-level synthesis
    Karfa, C.
    Mandal, C.
    Sarkar, D.
    Pentakota, S. R.
    Reade, Chris
    ISQED 2006: PROCEEDINGS OF THE 7TH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN, 2006, : 71 - +
  • [5] Formal verification of high-level conformance with symbolic simulation
    Kaivola, R
    Naik, A
    HLDVT'05: TENTH ANNUAL IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2005, : 153 - 159
  • [6] Utilizing high-level information for formal hardware verification
    Johannsen, P
    Drechsler, R
    ADVANCED COMPUTER SYSTEMS, PROCEEDINGS, 2002, 664 : 419 - 431
  • [7] Integration of high-level modeling, formal verification, and high-level synthesis in ATM switch design
    Rajan, SP
    Fujita, M
    ELEVENTH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 1997, : 552 - 557
  • [8] A new generation of ISCAS benchmarks from formal verification of high-level microprocessors
    Velev, MN
    2004 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOL 5, PROCEEDINGS, 2004, : 213 - 216
  • [9] Formal Verification of Optimizing Transformations during High-level Synthesis
    Chouksey, Ramanuj
    Karfa, Chandan
    Bhaduri, Purandar
    PROCEEDINGS OF THE 12TH INNOVATIONS ON SOFTWARE ENGINEERING CONFERENCE (ISEC), 2019,
  • [10] Comparative study of strategies for formal verification of high-level processors
    Velev, MN
    IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS & PROCESSORS, PROCEEDINGS, 2004, : 119 - 124
12345