A new generation of ISCAS benchmarks from formal verification of high-level microprocessors

被引：0
|
作者：
Velev, MN
机构：
来源：
2004 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOL 5, PROCEEDINGS | 2004年
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The paper presents a collection of 20 benchmark suites with a total of 1,132 ISCAS Boolean formulas from formal verification of high-level microprocessors, including pipelined, superscalar, and VLIW models with exceptions, multicycle functional units, branch prediction, instruction queues, and register renaming. These benchmarks can be used in research on testing, logic synthesis and optimization, equivalence verification, Decision Diagrams, and Boolean Satisfiability. The most complex formulas have more than 700,000 logic gates.
引用
收藏
页码：213 / 216
页数：4
相关论文
共 50 条
  • [1] High level formal verification of next-generation microprocessors
    Schubert, T
    40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 1 - 6
  • [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] 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 - +
  • [4] 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
  • [5] Utilizing high-level information for formal hardware verification
    Johannsen, P
    Drechsler, R
    ADVANCED COMPUTER SYSTEMS, PROCEEDINGS, 2002, 664 : 419 - 431
  • [6] 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
  • [7] 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,
  • [8] 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
  • [9] FEATURES OF HIGH-LEVEL LANGUAGES FOR MICROPROCESSORS
    DAVIES, AC
    MICROPROCESSORS AND MICROSYSTEMS, 1987, 11 (02) : 77 - 87
  • [10] HIGH-LEVEL LANGUAGE FOR EMBEDDED MICROPROCESSORS
    DAVIDSON, J
    MICROPROCESSORS AND MICROSYSTEMS, 1989, 13 (09) : 569 - 578
12345