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 条
  • [21] Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
    Charvat, Lukas
    Smrcka, Ales
    Vojnar, Tomas
    [J]. 2014 15TH INTERNATIONAL MICROPROCESSOR TEST AND VERIFICATION WORKSHOP (MTV 2014), 2015, : 83 - 89
  • [22] Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors
    Velev, MN
    [J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS, 2004, : 266 - 271
  • [23] The MODUS Approach to Formal Verification
    Brewka, Lukasz
    Soler, Jose
    Berger, Michael
    [J]. BUSINESS SYSTEMS RESEARCH JOURNAL, 2014, 5 (01): : 21 - 33
  • [24] The PERF Approach for Formal Verification
    Benaissa, Nazim
    Bonvoisin, David
    Feliachi, Abderrahmane
    Ordioni, Julien
    [J]. RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 203 - 214
  • [25] An easy approach to formal verification
    Schlipf, T
    Buchner, T
    Fritz, R
    Helms, M
    [J]. TENTH ANNUAL IEEE INTERNATIONAL ASIC CONFERENCE AND EXHIBIT, PROCEEDINGS, 1997, : 120 - 124
  • [26] Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction
    Velev, MN
    Bryant, RE
    [J]. 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 112 - 117
  • [27] Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors
    Velev, Miroslav N.
    Gao, Ping
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, 2010, 6447 : 355 - 370
  • [28] Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors
    Velev, MN
    Bryant, RE
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 2003, 35 (02) : 73 - 106
  • [29] Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors
    Velev, MN
    Bryant, RE
    [J]. 38TH DESIGN AUTOMATION CONFERENCE PROCEEDINGS 2001, 2001, : 226 - 231
  • [30] AN INFORMAL APPROACH TO FORMAL (ALGEBRAIC) SPECIFICATIONS
    FURTADO, AL
    MAIBAUM, TSE
    [J]. COMPUTER JOURNAL, 1985, 28 (01): : 59 - 67
12345