INCREMENTAL DESIGN AND FORMAL VERIFICATION OF MICROCODED MICROPROCESSORS

被引：0
|
作者：
HERBERT, JMJ
机构：
来源：
IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY | 1992年 / 10卷
关键词：
MATHEMATICAL LOGIC; CONTROL STRUCTURES AND MICROPROGRAMMING; MICROPROGRAM DESIGN AIDS; DEDUCTION AND THEOREM PROVING;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
A number of microprocessors have been specified and verified using machine supported formal techniques [2], [1], [7], [8], [10]. Some of these were pre-existing designs, others were designed as part of the specification and verification project. Even in the case of new designs, the formal techniques used offered very little support for incremental design and verification. Support for incremental design and verification means that certain additions to the implementation and/or specification can be verified without re-verification of the previous parts. Here, we present techniques for incremental design and verification which, as well as providing more appropriate models, also make the formal verification more efficient. The formal framework to support these ideas has been implemented in the HOL system and has been used in the specification, design and verification of a microcoded microprocessor. The techniques deal with three different aspects of the microprocessor: specification of machine instructions, modelling of microcode and modelling of bus architecture. For each of these, the techniques support incremental design and verification.
引用
收藏
页码：157 / 174
页数：18
相关论文
共 50 条
  • [11] Scalable formal verification methodology for pipelined microprocessors
    Levitt, Jeremy
    Olukotun, Kunle
    Proceedings - Design Automation Conference, 1996, : 558 - 563
  • [12] Formal verification of pipelined microprocessors with delayed branches
    Velev, Miroslav N.
    ISQED 2006: PROCEEDINGS OF THE 7TH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN, 2006, : 296 - 299
  • [13] Automatic Formal Verification of Multithreaded Pipelined Microprocessors
    Velev, Miroslav N.
    Gao, Ping
    2011 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2011, : 679 - 686
  • [14] A scalable formal verification methodology for pipelined microprocessors
    Levitt, J
    Olukotun, K
    33RD DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 1996, 1996, : 558 - 563
  • [15] Formal verification for microprocessors with extendable instruction set
    Sawitzki, S
    Spallek, RG
    Schönherr, J
    Straube, B
    IEEE INTERNATIONAL CONFERENCE ON APPLICATION-SPECIFIC SYSTEMS, ARCHITECTURES, AND PROCESSORS, PROCEEDINGS, 2000, : 47 - 55
  • [16] Balancing Automation and Control for Formal Verification of Microprocessors
    Goel, Shilpi
    Slobodova, Anna
    Sumners, Rob
    Swords, Sol
    COMPUTER AIDED VERIFICATION (CAV 2021), PT I, 2021, 12759 : 26 - 45
  • [17] Design verification of complex microprocessors
    Yim, J
    Park, C
    Yang, WS
    Oh, HS
    Choi, H
    Lee, S
    Won, N
    Park, IC
    Kyung, CM
    APCCAS '96 - IEEE ASIA PACIFIC CONFERENCE ON CIRCUITS AND SYSTEMS '96, 1996, : 441 - 448
  • [18] Design verification of complex microprocessors
    Yim, JS
    Park, CJ
    Park, IC
    Kyung, CM
    JOURNAL OF CIRCUITS SYSTEMS AND COMPUTERS, 1997, 7 (04) : 301 - 318
  • [19] Formal design verification for correctness of pipelined microprocessors with out-of-order instruction execution
    Takenaka, T
    Kitamichi, J
    Higashino, T
    Taniguchi, K
    PROCEEDINGS OF ASP-DAC '99: ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 1999, 1999, : 177 - 180
  • [20] Automated Debugging of Counterexamples in Formal Verification of Pipelined Microprocessors
    Velev, Miroslav N.
    Gao, Ping
    2012 17TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC), 2012, : 689 - 694
12345