## Sequential Equivalence Verification in the Sum State Space

Jie-Hong R. Jiang

(Professor Robert K. Brayton)

California State Micro program

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 M_{1} and M_{2} with numbers of
state variables m_{1} and m_{2} respectively, conventional formal
methods verify equivalence by traversing the state space of the
product machine, with m_{1} + m_{2} registers. In contrast, we
introduce a different possibility, based on partitioning the
state space defined by a multiplexed machine, which can have
merely max m_{1},m_{2} + 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.

Send mail to the author : (jiejiang@eecs.berkeley.edu)

Edit this abstract