Gate-level modelling and verification of asynchronous circuits using CSPM and FDR

被引：0
|
作者：
Josephs, Mark B. [1 ]
机构：
[1] London S Bank Univ, Fac BCIM, London, England
来源：
ASYNC 2007: 13TH IEEE INTERNATIONAL SYMPOSIUM ON ASYNCHRONOUS CIRCUITS AND SYSTEMS | 2007年
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
FDR (Failures-Divergences Refinement) is a tool for verifying properties of processes expressed in a machine-readable dialect of CSP (CSPM). This paper shows how to model asynchronous logic blocks as processes in CSPM and how to verify them using FDR: processes abstract away from the speed of the blocks; multi-way synchronization facilitates the modelling of isochronic forks; receptiveness is formalised as an assertion for FDR to check; process transformations allow one to model transmission lines and handshaking ports. A process parameterised by a Boolean function suffices to model any complex gate; another such process models N-way mutual exclusion. The approach is illustrated on a variety of asynchronous circuits drawn from the literature.
引用
收藏
页码：83 / 92
页数：10
相关论文
共 50 条
  • [1] Efficient verification of hazard-freedom in gate-level timed asynchronous circuits
    Nelson, CA
    Myers, CJ
    Yoneda, T
    [J]. ICCAD-2003: IEEE/ACM DIGEST OF TECHNICAL PAPERS, 2003, : 424 - 431
  • [2] Efficient verification of hazard-freedom in gate-level timed asynchronous circuits
    Nelson, Curtis A.
    Myers, Chris J.
    Yoneda, Tomohiro
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2007, 26 (03) : 592 - 605
  • [3] Design and Optimization of Asynchronous Circuits with Gate-level Pipelining
    Ikeda, Makoto
    [J]. PROCEEDINGS OF 2015 IEEE 11TH INTERNATIONAL CONFERENCE ON ASIC (ASICON), 2015,
  • [4] Verification of Gate-level Arithmetic Circuits by Function Extraction
    Ciesielski, Maciej
    Yu, Cunxi
    Brown, Walter
    Liu, Duo
    Rossi, Andre
    [J]. 2015 52ND ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2015,
  • [5] Self-referential verification for gate-level implementations of arithmetic circuits
    Chang, YT
    Cheng, KT
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2004, 23 (07) : 1102 - 1112
  • [6] Self-referential verification of gate-level implementations of arithmetic circuits
    Chang, YT
    Cheng, KT
    [J]. 39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002, 2002, : 311 - 316
  • [7] Gate-level simulation of quantum circuits
    Viamontes, GF
    Rajagopalan, M
    Markov, IL
    Hayes, JP
    [J]. ASP-DAC 2003: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2003, : 295 - 301
  • [8] POSET timing and its application to the synthesis and verification of gate-level timed circuits
    Myers, CJ
    Rokicki, TG
    Meng, THY
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1999, 18 (06) : 769 - 786
  • [9] Gate-level simulation of quantum circuits
    Viamontes, GF
    Rajagopalan, M
    Markov, IL
    Hayes, JP
    [J]. QUANTUM COMMUNICATION, MEASUREMENT AND COMPUTING, PROCEEDINGS, 2003, : 311 - 314
  • [10] Improving Gate-Level Simulation of Quantum Circuits
    Viamontes, George F.
    Markov, Igor L.
    Hayes, John P.
    [J]. QUANTUM INFORMATION PROCESSING, 2003, 2 (05) : 347 - 380
12345