Sequential equivalence checking without state space traversal

被引：29
|
作者：
van Eijk, CAJ [1 ]
机构：
[1] Eindhoven Univ Technol, Design Automat Sect, NL-5600 MB Eindhoven, Netherlands
来源：
DESIGN, AUTOMATION AND TEST IN EUROPE, PROCEEDINGS | 1998年
关键词：
D O I：
10.1109/DATE.1998.655922
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Because general algorithms for sequential equivalence checking require a state space traversal of the product machine, they are computationally expensive. In this paper; we present a new method for sequential equivalence checking which utilizes functionally equivalent signals to prove the equivalence of both circuits, thereby avoiding the state space traversal. The effectiveness of the proposed method is confirmed by experimental results on retimed and optimized ISCAS'89 benchmarks.
引用
收藏
页码：618 / 623
页数：6
相关论文
共 50 条
  • [31] Sequential Circuit Equivalence Checking Method Based on Minimizing Automation
    Gu, Yuwan
    Shi, Guodong
    Xie, Shiyan
    Sun, Yudiang
    ADVANCED RESEARCH ON INDUSTRY, INFORMATION SYSTEMS AND MATERIAL ENGINEERING, PTS 1-7, 2011, 204-210 : 251 - +
  • [32] Modified frame expansion based sequential equivalence checking algorithm
    ASIC and System State Key Laboratory, Microelectronics Department, Fudan University, Shanghai 200433, China
    Jisuanji Fuzhu Sheji Yu Tuxingxue Xuebao, 2006, 1 (53-61):
  • [33] Matching in the presence of don't cares and redundant sequential elements for sequential equivalence checking
    Rahim, S
    Rouzeyre, B
    Torres, L
    Rampon, J
    EIGHTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2003, : 129 - 134
  • [34] Generation of the Path to Counter-Examples by Backward State Space Traversal in Symbolic Model Checking Based on Term Rewriting
    Pura, Mihai Lica
    Morogan, Luciana
    Buchs, Didier
    2016 INTERNATIONAL CONFERENCE ON COMMUNICATIONS (COMM 2016), 2016, : 85 - 88
  • [35] Sequential circuit test generation using dynamic state traversal
    Hsiao, MS
    Rudnick, EM
    Patel, JH
    EUROPEAN DESIGN & TEST CONFERENCE - ED&TC 97, PROCEEDINGS, 1997, : 22 - 28
  • [36] Automatic decomposition for sequential equivalence checking of system level and RTL descriptions
    Vasudevan, Shobha
    Viswanath, Vinod
    Abraham, Jacob A.
    Tu, Jiajin
    FOURTH ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2006, : 71 - +
  • [37] On sequential traversal of sets
    Chentsov, A. G.
    Chentsov, P. A.
    VESTNIK UDMURTSKOGO UNIVERSITETA-MATEMATIKA MEKHANIKA KOMPYUTERNYE NAUKI, 2021, 31 (03): : 487 - 504
  • [38] Leveraging sequential equivalence checking to enable system-level to RTL flows
    Urard, Pascal
    Maalej, Asma
    Guizzetti, Roberto
    Chawla, Nitin
    Krishnaswamy, Venkatram
    2008 45TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2008, : 816 - 821
  • [39] Using Range-equivalent Circuits for Facilitating Bounded Sequential Equivalence Checking
    Chen, Yung-Chih
    Ji, Wei-An
    Wang, Chih-Chung
    Huang, Ching-Yi
    Wu, Chia-Cheng
    Lin, Chia-Chun
    Wang, Chun-Yao
    2018 INTERNATIONAL SYMPOSIUM ON VLSI DESIGN, AUTOMATION AND TEST (VLSI-DAT), 2018,
  • [40] Mining global constraints with domain knowledge for improving bounded sequential equivalence checking
    Wiu, Weixin
    Hsiao, Michael S.
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2008, 27 (01) : 197 - 201
12345