https://scholars.lib.ntu.edu.tw/handle/123456789/304395
Title: | On the Verification of Sequential Equivalence | Authors: | JIE-HONG JIANG Robert K. Brayton |
Keywords: | Binary decision diagram (BDD); Equivalence checking; Formal verification; Sequential machines; Symbolic techniques | Issue Date: | Jun-2003 | Journal Volume: | 22 | Journal Issue: | 6 | Start page/Pages: | 686-697 | Source: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | Abstract: | The state-explosion problem limits formal verification on large sequential circuits partly because the sizes of binary decision diagrams (BDDs) sizes heavily depend on the number of variables dealt with. In the worst case, a BDD size grows exponentially with the number of variables. Thus, reducing this number can possibly increase the verification capacity. In particular, this paper shows how sequential equivalence checking can be done in the sum state space. Given two finite state machines M1 and M2 with numbers of state variables m1 and m2, respectively, conventional formal methods verify equivalence by traversing the state space of the product machine with m1 + m2 registers. In contrast, this paper introduces a different possibility, based on partitioning the state space defined by a multiplexed machine, which can have merely max {m1, m2} + 1 registers. This substantial reduction in state variables potentially enables the verification of larger instances. Experimental results show the approach can verify benchmarks with up to 312 registers, including all of the control outputs of microprocessor 8085. |
URI: | http://scholars.lib.ntu.edu.tw/handle/123456789/304395 https://www.scopus.com/inward/record.uri?eid=2-s2.0-0038718553&doi=10.1109%2fTCAD.2003.811446&partnerID=40&md5=f5d7cb84d1f171806731d403ea998d97 |
ISSN: | 02780070 | DOI: | 10.1109/TCAD.2003.811446 | SDG/Keyword: | Computational methods; Microprocessor chips; Problem solving; Sequential machines; Binary decision diagrams (BDD); Computer aided design |
Appears in Collections: | 電子工程學研究所 |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.