Efficient state representation for symbolic simulation

Symbolic simulation is attracting increasing interest for the validation of digital circuits. It allows the verification engineer to explore all, or a major portion of the circuit´s state space without having to design specific and time-consuming test stimuli. However, the complexity and unpredictable run-time behavior of symbolic simulation have limited its scope to small-to-medium circuits. In this paper, we propose a novel approach to symbolic simulation that reduces the size of the BDDs of the state vector while maintaining an exact representation of the set of states visited. The method exploits the decomposition properties of Boolean functions. By restructuring the next-state functions in their disjoint support components, we gain a better insight in the role of each input variable. Consequently, we can simplify the next-state functions without significantly sacrificing the simulation accuracy. Our experimental results shows that this approach can be used in effectively reducing the memory requirements of symbolic simulation while surrendering only a small portion of the design´s state space.