An algebraic approach to formal verification of microprocessors

被引：0
|
作者：
Hirabayashi, K [1 ]
机构：
[1] Toshiba Techno Ctr Inc, Tokyo 1050013, Japan
来源：
JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS | 2001年 / 17卷 / 06期
关键词：
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 条
  • [21] Efficient translation of boolean formulas to CNF in formal verification of microprocessors
    Velev, MN
    ASP-DAC 2004: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2004, : 310 - 315
  • [22] Formal Verification and Debugging of Precise Interrupts on High Performance Microprocessors
    Alizadeh, Bijan
    ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2012, 17 (04)
  • [23] Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
    Charvat, Lukas
    Smrcka, Ales
    Vojnar, Tomas
    2014 15TH INTERNATIONAL MICROPROCESSOR TEST AND VERIFICATION WORKSHOP (MTV 2014), 2015, : 83 - 89
  • [24] Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors
    Velev, MN
    DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS, 2004, : 266 - 271
  • [25] The MODUS Approach to Formal Verification
    Brewka, Lukasz
    Soler, Jose
    Berger, Michael
    BUSINESS SYSTEMS RESEARCH JOURNAL, 2014, 5 (01): : 21 - 33
  • [26] The PERF Approach for Formal Verification
    Benaissa, Nazim
    Bonvoisin, David
    Feliachi, Abderrahmane
    Ordioni, Julien
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 203 - 214
  • [27] An easy approach to formal verification
    Schlipf, T
    Buchner, T
    Fritz, R
    Helms, M
    TENTH ANNUAL IEEE INTERNATIONAL ASIC CONFERENCE AND EXHIBIT, PROCEEDINGS, 1997, : 120 - 124
  • [28] Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction
    Velev, MN
    Bryant, RE
    37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 112 - 117
  • [29] Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors
    Velev, Miroslav N.
    Gao, Ping
    FORMAL METHODS AND SOFTWARE ENGINEERING, 2010, 6447 : 355 - 370
  • [30] Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors
    Velev, MN
    Bryant, RE
    JOURNAL OF SYMBOLIC COMPUTATION, 2003, 35 (02) : 73 - 106
12345