The state explosion problem limits formal verification on large sequential circuits partly because BDD sizes heavily depend on the number of variables dealt with. In the worst case, a BDD size grows exponentially with the number of variables. Reducing this number can possibly enlarge the verification capacity. In particular, we show 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, we introduce 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.
We are currently exploring techniques to extend the verification capacity. One possiblity would be using output transformation such that equivalence classes of states induced by the new outputs are reduced and amortized. Another would be using structure similarities between two sequential circuits to reduce the verification complexity. In addition, we are investigating how to make our verification approach more scalable especially for high performance IC design methodologies.