TRANS: Efficient sequential verification of loop-free circuits

被引：0

作者：

Khasidashvili, Z ^{[1
]}

Moondanos, J ^{[1
]}

Hanna, Z ^{[1
]}

机构：

[1] Intel, IDC, Log & Validat Technol Design Technol Div, Haifa, Israel

来源：

SEVENTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS | 2002年

关键词：

D O I：

10.1109/HLDVT.2002.1224439

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Bischoff et al [2] proposed a method for reducing sequential verification of loop-free circuits to combinational verification, by constructing and comparing the so called Timed (ternary) Binary Decision Diagrams (TBDDs). Ranjan et al [8] independently re-discovered a similar method. Here we propose a much more simple and efficient algorithm for constructing TBDDs. Furthermore, we prove the soundness of the algorithm, and describe very briefly a (restricted) new algorithm for generating sequential counter examples. These algorithms are implemented in Intel's sequential verification engine, TRANS.

引用

页码：115 / 120

页数：6

共 50 条

[1] LOOP-FREE STRUCTURE OF SEQUENTIAL MACHINES
HARTMANIS, J
[J]. INFORMATION AND CONTROL, 1962, 5 (01): : 25 - &
[2] Efficient computation of loop-free alternates
Geng, Haijun
Zhang, Han
Shi, Xingang
Wang, Zhiliang
Yin, Xia
[J]. JOURNAL OF NETWORK AND COMPUTER APPLICATIONS, 2020, 151
[3] ANALYSIS OF CIRCUITS WITH SWITCHABLE CONDENSERS BY THE ORIENTED LOOP-FREE GRAPH
KOROTKOV, AS
[J]. IZVESTIYA VYSSHIKH UCHEBNYKH ZAVEDENII RADIOELEKTRONIKA, 1994, 37 (11-12): : 68 - 72
[4] Efficient Loop-Free Rerouting of Multiple SDN Flows
Basta, Arsany
Blenk, Andreas
Dudycz, Szymon
Ludwig, Arne
Schmid, Stefan
[J]. IEEE-ACM TRANSACTIONS ON NETWORKING, 2018, 26 (02) : 948 - 961
[5] A More Efficient Diffusing Update Algorithm For Loop-Free Routing
Zhao, Chuanqiang
Liu, Yuanan
Liu, Kaiming
[J]. 2009 5TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS, NETWORKING AND MOBILE COMPUTING, VOLS 1-8, 2009, : 4081 - 4084
[6] Message-efficient dissemination for loop-free centralized routing
Peterson, Haldane
Sen, Soumya
Chandrashekar, Jaideep
Gao, Lixin
Guerin, Roch
Zhang, Zhi-Li
[J]. ACM SIGCOMM COMPUTER COMMUNICATION REVIEW, 2008, 38 (03) : 65 - 74
[7] Simple and Efficient Loop-Free Multipath Routing in Wireless Networks
Garcia-Luna-Aceves, J. J.
Cirimelli-Low, Dylan J.
[J]. PROCEEDINGS OF THE INT'L ACM CONFERENCE ON MODELING, ANALYSIS AND SIMULATION OF WIRELESS AND MOBILE SYSTEMS, MSWIM 2023, 2023, : 47 - 56
[8] Synthesis of Loop-free Programs
Gulwani, Sumit
Jha, Susmit
Tiwari, Ashish
Venkatesan, Ramarathnam
[J]. PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2011, : 62 - 73
[9] Path verification for robust, instantaneous loop-free routing in ad hoc networks
Rangarajan, H
Garcia-Luna-Aceves, JJ
[J]. 2005 IEEE Wireless Communications and Networking Conference, Vols 1-4: WCNC 2005: BROADBAND WIRELESS FOR THE MASSES READY FOR TAKE-OFF., 2005, : 2014 - 2019
[10] Synthesis of Loop-free Programs
Gulwani, Sumit
Jha, Susmit
Tiwari, Ashish
Venkatesan, Ramarathnam
[J]. ACM SIGPLAN NOTICES, 2011, 46 (06) : 62 - 73

← 1 2 3 4 5 →