2D Decomposition Sequential Equivalence Checking of System Level and RTL Descriptions

Dan Zhu,  Tun Li,  Yang Guo,  Si-kun Li
School of Computer Science and Technology, National University of Defense Technology


Symbolic simulation-based approach is viable for the sequential equivalence checking of SLM-vs.-RTL. However, it can’t avoid the storage explosion introduced by the explosion of the BDD sizes for large designs. For scalability, we introduce two kinds of decomposition techniques: One is the equivalence checking oriented program slicing; the other is the hierarchical insertion of logic cutpoints. And a 2D decomposition sequential equivalence checking method of SLM-vs.-RTL is presented.”2D decomposition” means decomposition in the space dimension and the time dimension. The verification model is only built for the program slices of a single output variable for each time, which limits the usage of memory. During checking the equivalence of the program slices, the logic cutpoints are inserted to split the verification model of the program slices in the time dimension, which controls the storage explosion further. The promising experimental results demonstrate the benefits brought by our approach.