Formal verification of peephole optimizations in asynchronous circuits

被引：0
|
作者：
Kong, XH [1 ]
Negulescu, R [1 ]
机构：
[1] McGill Univ, Dept Elect & Comp Engn, Montreal, PQ H3A 2A7, Canada
来源：
FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS | 2001年 / 69卷
关键词：
peephole optimization; formal verification; peephole rule; relative timing; process spaces;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper proposes and applies novel techniques for formal verification of peephole optimizations in asynchronous circuits. We verify whether locally optimized modules can replace parts of an existing circuit under assumptions regarding the operation of the optimized modules in context. A verification rule related to assume-guarantee and hierarchical, verification is presented, using relative timing constraints as optimization assumptions. We present the verification of speed-optimizations in an asynchronous arbiter as a case study.
引用
收藏
页码：219 / 234
页数：16
相关论文
共 50 条
  • [1] Practical Verification of Peephole Optimizations with Alive
    Lopes, Nuno P.
    Menendez, David
    Nagarakatte, Santosh
    Regehr, John
    COMMUNICATIONS OF THE ACM, 2018, 61 (02) : 84 - 91
  • [2] Formal Modeling and Verification of PCHB Asynchronous Circuits
    Sakib, Ashiq A.
    Smith, Scott C.
    Srinivasan, Sudarshan K.
    IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2019, 27 (12) : 2911 - 2924
  • [3] Formal verification of pulse-mode asynchronous circuits
    Kong, XH
    Negulescu, R
    PROCEEDINGS OF THE ASP-DAC 2001: ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 2001, 2001, : 347 - 352
  • [4] Automatic optimization techniques for formal verification of asynchronous circuits
    Boubekeur, M.
    Schellekens, M. P.
    2007 14TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS, VOLS 1-4, 2007, : 283 - 286
  • [5] Towards Formal Verification of Reset Sequence in Fully Asynchronous Digital Circuits
    Melnychenko, Oleksandr
    Kreuter, Hans-Peter
    2014 10TH CONFERENCE ON PH.D. RESEARCH IN MICROELECTRONICS AND ELECTRONICS (PRIME 2014), 2014,
  • [6] Verified Peephole Optimizations for CompCert
    Mullen, Eric
    Zuniga, Daryl
    Tatlock, Zachary
    Grossman, Dan
    ACM SIGPLAN NOTICES, 2016, 51 (06) : 448 - 461
  • [7] A Framework for Formal Verification of Compiler Optimizations
    Mansky, William
    Gunter, Elsa
    INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 371 - 386
  • [8] Automatic generation of peephole optimizations
    Davidson, JW
    Fraser, CW
    ACM SIGPLAN NOTICES, 2004, 39 (04) : 104 - 105
  • [9] AUTOMATIC-GENERATION OF PEEPHOLE OPTIMIZATIONS
    DAVIDSON, JW
    FRASER, CW
    SIGPLAN NOTICES, 1984, 19 (06): : 111 - 116
  • [10] AUTOMATIC VERIFICATION OF ASYNCHRONOUS CIRCUITS
    CLARKE, E
    MISHRA, B
    LECTURE NOTES IN COMPUTER SCIENCE, 1984, 164 : 101 - 115
12345