https://scholars.lib.ntu.edu.tw/handle/123456789/304395
標題: | On the Verification of Sequential Equivalence | 作者: | JIE-HONG JIANG Robert K. Brayton |
關鍵字: | Binary decision diagram (BDD); Equivalence checking; Formal verification; Sequential machines; Symbolic techniques | 公開日期: | 六月-2003 | 卷: | 22 | 期: | 6 | 起(迄)頁: | 686-697 | 來源出版物: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | 摘要: | 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/關鍵字: | Computational methods; Microprocessor chips; Problem solving; Sequential machines; Binary decision diagrams (BDD); Computer aided design |
顯示於: | 電子工程學研究所 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。