Symbolic simulation-based approach is viable for the sequential equivalence checking (SEC) 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 SEC 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 2D decomposition method.
展开▼
