Achieving scalable hardware verification with symbolic simulation
Kunle Olukotun, Valeria Bertacco · 2003
In recent years, the complexity of digital integrated circuit (IC) designs has grown at a challenging pace. Within this context, proper verification of an IC design has become a central aspect of the development cycle. Logic simulation is the accepted method for verification because of its scalability, although it can only visits a small fraction of the state space. Symbolic simulation is an alternative method that is attracting increasing interest because it can explore a major portion of the circuit's state space without the need of design-specific tests. The limiting factor to the mainstream deployment of this approach has been its complexity and unpredictable run-time behavior. This thesis presents two new symbolic simulation based approaches to the verification problem that radically improve scalability and narrow the performance gap between design complexity and verification. The first technique, Cycle-Based Symbolic Simulation, is a unique combination of formal methods and logic simulation to stimulate a circuit with a very large number of input combinations in parallel through the use of a parametric form. This approach maintains a high degree of scalability while achieving better efficiency than logic simulation. To better exploit the use of parameterization, Disjoint Support Decomposition Based Symbolic Simulation, our second technique, exploits the disjoint support decomposition (DSD) properties of the state functions. We develop a new algorithm that exposes the DSD of a Boolean function by restructuring its BDD representation. The new algorithm is very efficient in the sense that it has worst-case complexity that is only quadratic in the size of the initial BDD. We deployed this algorithm to find the DSD of the state functions in symbolic simulation, which we then use to generate a more compact, but exact, parametric form. Both of these techniques have been tested on the ISCAS and Logic Synthesis benchmark suites. The results show that the first technique can simulate very large trace sets in parallel, maintaining a simulation speed and memory profile that are much closer to logic simulation. The second technique is effective in reducing the memory requirements of symbolic simulation while preserving an exact state exploration.