An algebraic approach to formal verification of microprocessors

被引:0
|
作者
Hirabayashi, K [1 ]
机构
[1] Toshiba Techno Ctr Inc, Tokyo 1050013, Japan
关键词
formal verification; microprocessor;
D O I
10.1023/A:1012824822961
中图分类号
TM [电工技术]; TN [电子技术、通信技术];
学科分类号
0808 ; 0809 ;
摘要
In this letter we report the formal verification of microprocessors. After we describe algebraically a bit-sliced microprocessor at both function and logic levels, we apply the symbolic manipulation of Mathematica.
引用
收藏
页码:543 / 544
页数:2
相关论文
共 50 条
  • [1] An Algebraic Approach to Formal Verification of Microprocessors
    Kanji Hirabayashi
    [J]. Journal of Electronic Testing, 2001, 17 : 543 - 544
  • [2] FORMAL VERIFICATION OF MICROPROCESSORS
    SRIVAS, M
    BICKFORD, M
    [J]. COMPASS 89 : PROCEEDINGS OF THE FOURTH ANNUAL CONFERENCE ON COMPUTER ASSURANCE: SYSTEMS INTEGRITY, SOFTWARE SAFETY AND PROCESS SECURITY, 1989, : 93 - 102
  • [3] A methodology for the formal verification of RISC microprocessors - A functional approach
    Merniz, S.
    Benmohammed, M.
    [J]. 2007 IEEE/ACS INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS, VOLS 1 AND 2, 2007, : 492 - +
  • [4] FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS
    WINDLEY, PJ
    [J]. IEEE TRANSACTIONS ON COMPUTERS, 1995, 44 (01) : 54 - 72
  • [5] Formal verification of explicitly parallel microprocessors
    Cook, B
    Launchbury, J
    Matthews, J
    Kieburtz, D
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 23 - 36
  • [6] Formal verification of iterative algorithms in microprocessors
    Aagaard, MD
    Jones, RB
    Kaivola, R
    Kohatsu, KR
    Seger, CJH
    [J]. 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 201 - 206
  • [7] Abstract modeling and formal verification of microprocessors
    Hanna, Ziyad
    [J]. Computer Science - Theory and Applications, 2007, 4649 : 23 - 23
  • [8] A scalable formal verification methodology for pipelined microprocessors
    Levitt, J
    Olukotun, K
    [J]. 33RD DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 1996, 1996, : 558 - 563
  • [9] Automatic Formal Verification of Multithreaded Pipelined Microprocessors
    Velev, Miroslav N.
    Gao, Ping
    [J]. 2011 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2011, : 679 - 686
  • [10] INCREMENTAL DESIGN AND FORMAL VERIFICATION OF MICROCODED MICROPROCESSORS
    HERBERT, JMJ
    [J]. IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1992, 10 : 157 - 174