Enhanced symbolic simulation for verification of embedded memory systems and datapaths

With the ever increasing complexity of digital integrated systems, the verification becomes the bottleneck in the design flow and the problem has been exacerbated by the reduced times-to-market. The modern VLSI design becomes data-intensive in nature. Much data needs to be stored on-chip and computed with complex algorithms to achieve the high-performance applications. The embedded memory systems and datapaths occupy the majority of areas in the full-chip design. Both of them have been shown the difficulty in verification.; OBDD-based symbolic simulation is a powerful engine with unique advantages to target the embedded memory systems and datapaths. However, it is easy for OBDD to suffer from the memory space explosion problem. A symbolic simulator with effective, robust and generic methods is urgently needed for the modern VLSI designs.; In this dissertation, we have developed an enhanced symbolic simulator which incorporated a universal data structure (called 2-tuple list). Several techniques are applied for the symbolic simulation to effectively avoid the OBDD size explosion. It includes the symbolic encoding, OBDD decomposition for equality function and OBDD partitioning. There is one critical concept as a thread to connect the entire dissertation: the exploration of critical "control" signals for verification. The control signals are related to the important properties of the data flow in the memory systems and datapaths. These control signals exist in the high-level behavioral descriptions and can be implemented in the RT-level, gate-level or transistor-level netlist. They can also implicitly exist in the OBDD representations. The control signals are very important to improve the efficiency of symbolic simulation. They are used in case splitting to apply the symbolic encoding. They are also used to partition a monolithic OBDD into several OBDDs at the decision points. For the datapath operators, the control signals are helpful to determine the optimal OBDD variable ordering. In the equivalence checking of two datapath circuits, we used the circuit re-structure approaches to recover the control signals and increase the similarity of two circuits under comparison.; We will discuss the methods in detail to extract and make use of the control signals in the symbolic simulation. The embedded memory systems such as the memory management unit and the datapath designs such as the floating point adder and arithmetic operators are verified with our symbolic simulator.