On the verification of sequential equivalence

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 M₁ and M₂ with numbers of state variables m₁ and m₂, respectively, conventional formal methods verify equivalence by traversing the state space of the product machine with m₁+m₂ 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{m₁,m₂}+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.