| In recent years, verification has emerged as a major portion of the effort in designing large, complex chips. Simulation-based methods such as directed and random testing are the most widely used verification methods today. However, there is growing concern that simulation will not be able to keep up with increased design sizes in the future. Research into better verification methods has focussed on symbolic methods such as model checking. These methods have had success in augmenting simulation, but, so far, have not been able to replace simulation as the primary verification method.; This thesis proposes using symbolic simulation as a replacement for directed and random simulation in the verification of large, system-level designs. Symbolic simulation allows many directed tests to be combined into a single symbolic test. This reduces the effort of executing a test plan, often the bottleneck in verification. Directed and random testing are predictable and easy to use and so find most of the bugs in designs today. Conventional symbolic simulation lacks this level of usability due to the use of Binary Decision Diagrams (BDDs), which can overflow memory unpredictably, to represent symbolic values.; This problem is addressed by allowing the symbolic simulator to automatically BDD overflow, and second, it mitigates overflow when it happens. To reduce the probability of overflow, don't care values are identified during simulation and are replaced with values that have smaller representations. Don't care values are identified by classifying symbolic variables in the test as either care or don't care variables. BDD overflow is mitigated using satisfiability checking (SAT) methods, which can prove a property true or false without requiring additional memory at the cost of using additional execution time. The effectiveness of these techniques is demonstrated on realistic industrial designs. |
