On using a 2-domain partitioned OBDD data structure in verification

In this paper, we propose a symbolic simulation method where Boolean functions can be efficiently manipulated through a 2-domain partitioned OBDD data structure. The functional partition is applied based on the key decision points in a circuit. We demonstrate that key decision points in an RTL model can be extracted automatically to facilitate verification at the gate level. The experiments show that the decision points can help to significantly reduce the OBDD size in both RTL and gate level circuit, solving problems that could not be solved with monolithic OBDD data structure. The performance of 2-domain partitioned OBDD approach is shown through the verification of several benchmark circuits.