Achieving Scalable Hardware Verification with Symbolic Simulation

Valeria Bertacco
Ph.D. Dissertation, Stanford University
August 2003

Abstract

In the past 40 years, electronic systems have become pervasive in modern society. Digital integrated circuits (ICs) are at the heart of the large majority of these systems. These digital ICs are complex systems containing millions of interconnected transistors in a very small area. Moreover, the underlying semiconductor fabrication technology used to fabricate these ICs allows doubling the number of transistors in the same area approximately every 18 months.

The design of digital systems is a complex and time consuming process that progresses through various phases and levels of abstraction, and relies heavily on CAD (Computer-Aided Design) software tools. Within this context, ensuring the correctness of these digital systems is a major consideration, especially because the cost of failures is becoming increasingly high. One of the most famous recent examples of its importance is the Intel, Inc. Pentium's flaw in the floating point divide unit of 1994 that eventually forced Intel to replace all the Pentium chips that were already in the market. In many cases, the possibility of failure is even unacceptable, examples of these applications are: transportation systems, medical applications and financial systems. Even though guaranteeing the correctness of a design is such a central aspect in its development, current verification methodologies are still inadequate to tackle the complex systems that are being developed nowadays. Hardware design companies try to compensate for mediocre CAD tools by dedicating the majority of their resources involved in a design to verification, yet are still unable to guarantee correct functionality over the entire design space.

Logic simulation is the most widely accepted method for ensuring the correctness of digital ICs in industry because of its scalability, flexibility and predictable run-time behavior. This technique is based on verifying a digital system by providing sequences of binary values for each of the inputs of the system and checking that the corresponding outputs are correct, based on what the design team expected or described in a specification document. However, because of its inherent approach, this validation technique usually can visit only a small fraction of all the possible configurations of a system - also called the state space - and thus the discovery of bugs heavily relies on the expertise of the designer of the test stimuli to select a few crucial configurations to verify. Symbolic simulation is another verification method that is attracting increasing interest because it allows the verification engineer to explore all, or a major portion, of a circuit's state space without the need to design time-consuming test stimuli. However, this approach poses a high demand on the resources of the simulating host, and in particular, on the memory system, because of the complexity of the algorithms involved and their unpredictable run-time behavior. Thus, the scalability of this approach has been the main limiting factor to its mainstream deployment and so far its scope has been limited to small systems.

This thesis presents new symbolic simulation based approaches to the verification problem that radically improve scalability. We present two new techniques that narrow the performance gap between the complexity of digital systems that are being developed and the limited ability to verify them. The first technique, Cycle-Based Symbolic Simulation, is a unique combination of formal methods and logic simulation that can stimulate a circuit with a very large number of input combinations and sequences in parallel. The key concept is the use of a parametric form to represent the set of states visited during simulation. This approach maintains a high degree of scalability, in line with current cycle-based logic simulation techniques, while achieving better efficiency. To better exploit the use of parameterization in improving the memory profile of simulation, the second technique, Disjoint Support Decomposition Based Symbolic Simulation, exploits the disjoint support of decomposition properties of the state functions. We develop a new algorithm that exposes the disjoint decomposition properties 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, while previous algorithms had exponential complexity in the size of the function's support. We deployed this algorithm to find the disjoint support decomposition of the state functions in symbolic simulation. By restructuring the next-state functions using their disjoint support components, it is possible to gain better insight about the role of each input variable. Consequently, the next-state functions can be transformed into a simpler parametric form without sacrificing simulation accuracy. Both of these techniques have been tested on the ISCAS benchmark suite. 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 maintaining exact state exploration.