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 条
  • [1] Formal Design and Verification of Memory Management Unit Microprocessor
    Yang, Hongwei
    Ma, Dianfu
    [J]. 2019 IEEE 2ND INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATION ENGINEERING TECHNOLOGY (CCET), 2019, : 124 - 128
  • [2] FORMAL VERIFICATION OF A PIPELINED MICROPROCESSOR
    SRIVAS, M
    BICKFORD, M
    [J]. IEEE SOFTWARE, 1990, 7 (05) : 52 - 64
  • [3] Formal verification of a microprocessor control
    Ivanov, L
    [J]. PROCEEDINGS OF THE 44TH IEEE 2001 MIDWEST SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOLS 1 AND 2, 2001, : 646 - 650
  • [4] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    [J]. INTEGRATION-THE VLSI JOURNAL, 1989, 7 (03) : 247 - 266
  • [5] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1988, 24 (1-5): : 371 - 378
  • [6] FORMAL VERIFICATION - IS IT PRACTICAL FOR REAL-WORLD DESIGN
    CAMURATI, P
    CHIN, SK
    FOURMAN, M
    PRINETTO, P
    TAKAHARA, A
    [J]. IEEE DESIGN & TEST OF COMPUTERS, 1989, 6 (06): : 50 - 58
  • [7] FORMAL ASPECTS OF MICROPROCESSOR DESIGN
    HUSSEIN, Z
    [J]. MICROPROCESSORS AND MICROSYSTEMS, 1990, 14 (10) : 621 - 622
  • [8] THE PRACTICAL APPLICATION OF FORMAL VERIFICATION
    BEENKER, GFM
    CLAESEN, L
    EVEKING, H
    FUJITA, M
    ODDO, P
    [J]. IEEE DESIGN & TEST OF COMPUTERS, 1995, 12 (03): : 96 - 102
  • [9] Formal Verification of Practical MPI Programs
    Vo, Anh
    Vakkalanka, Sarvani
    DeLisi, Michael
    Gopalakrishnan, Ganesh
    Kirby, Robert M.
    Thakur, Rajeev
    [J]. ACM SIGPLAN NOTICES, 2009, 44 (04) : 261 - 269
  • [10] Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems
    Charvat, Lukas
    Smrcka, Ales
    Vojnar, Tomas
    [J]. COMPUTER AIDED SYSTEMS THEORY - EUROCAST 2015, 2015, 9520 : 605 - 614
12345