On the Verification of Sequential Equivalence
Journal
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Journal Volume
22
Journal Issue
6
Pages
686-697
Date Issued
2003-06
Author(s)
Robert K. Brayton
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.
Subjects
Binary decision diagram (BDD); Equivalence checking; Formal verification; Sequential machines; Symbolic techniques
SDGs
Other Subjects
Computational methods; Microprocessor chips; Problem solving; Sequential machines; Binary decision diagrams (BDD); Computer aided design
Type
conference paper