Practical formal verification in microprocessor design

被引：21
|
作者：
Jones, RB
O'Leary, JW
Seger, CJH
Aagaard, MD
Melham, TF
机构：
[1] Intel Corp, Strateg CAD Labs, Hillsboro, OR 97123 USA
[2] Univ Waterloo, Dept Elect & Comp Engn, Waterloo, ON N2L 3G1, Canada
[3] Univ Glasgow, Glasgow G12 8QQ, Lanark, Scotland
来源：
IEEE DESIGN & TEST OF COMPUTERS | 2001年 / 18卷 / 04期
关键词：
D O I：
10.1109/54.936245
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Practical application of formal methods requires more than advanced technology and tools; it requires an appropriate methodology, A verification methodology for data-path-dominated hardware combines model checking and theorem proving in a customizable framework. This methodology has been effective in large-scale industrial trials, including verification of an IEEE-compliant floating-point adder.
引用
收藏
页码：16 / 25
页数：10
相关论文
共 50 条
  • [21] Practical methods in Coverage-Oriented verification of the Merom microprocessor
    Gluska, Alon
    43rd Design Automation Conference, Proceedings 2006, 2006, : 332 - 337
  • [22] Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods
    Srivas, MK
    Miller, SP
    FORMAL METHODS IN SYSTEM DESIGN, 1996, 8 (02) : 153 - 188
  • [23] Control and data abstraction: The cornerstones of practical formal verification
    Kesten Y.
    Pnueli A.
    International Journal on Software Tools for Technology Transfer, 2000, 2 (04) : 328 - 342
  • [24] Design and formal verification of an intelligent alarm
    Li, Xin Ben
    Sun, De Chao
    WSEAS Transactions on Systems, 2007, 6 (03): : 576 - 581
  • [25] FORMAL DESIGN VERIFICATION OF DIGITAL CIRCUITRY
    BUTLER, RW
    SJOGREN, JA
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 1991, 32 (1-2) : 67 - 93
  • [26] Formal System Design and Verification: A Perspective
    Rajamani, Sriram
    ISOFT: PROCEEDINGS OF THE 13TH INNOVATIONS IN SOFTWARE ENGINEERING CONFERENCE, 2020,
  • [27] Getting formal verification into design flow
    Arvind, S.
    Dave, Nirav
    Katelman, Michael
    FM 2008: FORMAL METHODS, PROCEEDINGS, 2008, 5014 : 12 - +
  • [28] Formal verification in intel CPU design
    O'Leary, J
    Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2004, : 152 - 152
  • [29] DESIGN OF A FORMAL ESTELLE SEMANTICS FOR VERIFICATION
    BREDEREKE, J
    GOTZHEIN, R
    VOGT, FH
    IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS, 1993, 10 : 153 - 168
  • [30] Assured VLSI design with formal verification
    Kim, JD
    Chin, SK
    COMPASS '97 - ARE WE MAKING PROGRESS TOWARDS COMPUTER ASSURANCE?, 1997, : 13 - 22
12345