An Algebraic Approach to Formal Verification of Microprocessors

被引：0
|
作者：
Kanji Hirabayashi
机构：
[1] Toshiba Techno Center Inc.,
来源：
Journal of Electronic Testing | 2001年 / 17卷
关键词：
formal verification; microprocessor;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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
页数：1
相关论文
共 50 条
  • [1] An algebraic approach to formal verification of microprocessors
    Hirabayashi, K
    [J]. JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS, 2001, 17 (06): : 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 REWRITING BASED METHOD FOR THE FORMAL VERIFICATION OF MICROPROCESSORS
    ALLEMAND, M
    [J]. COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 115 - 122
  • [9] Formal verification of pipelined microprocessors with delayed branches
    Velev, Miroslav N.
    [J]. ISQED 2006: PROCEEDINGS OF THE 7TH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN, 2006, : 296 - 299
  • [10] 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
12345