Report Number: CSL-TR-96-708
Institution: Stanford University, Computer Systems Laboratory
Title: Validation Tools for Complex Digital Designs
Author: Ho, Chian-Min Richard
Date: December 1996
Abstract: The functional validation of a complex digital design is a laborious, ad-hoc and open-ended task. Many circuits are too complex to be formally verified in their entirety. Instead, simulation of a register transfer level (RTL) model is used. This research explores techniques to make the validation task more systematic, automated and efficient. This can be accomplished by using information embedded in the RTL model to extract the set of "interesting behaviors" of the design, represented as interacting finite state machines (FSM). If all such interesting behaviors of the RTL could be tested in simulation, the degree of confidence that the design is correct would be substantially higher. This work provides two tools towards this goal. First, a test vector generator is described that uses this information to produce a series of test vectors that exercise all the implemented behaviors of the design in RTL simulation. Secondly, the information can be used as the basis for coverage analysis of a pre-existing test vector suite. Previous coverage metrics, such as toggles on a node in the circuit or code block execution counts, often give good first order indications of how thorough a circuit has been exercised but do not usually give an accurate picture of whether multiple or concurrent events have been exercised. In this thesis, a new method is proposed of analyzing test vector suite coverage based on projecting a minimized control state graph onto control signals that enter the datapath part of the design. The fundamental problem facing any technique that uses state exploration is state space explosion. Two techniques are proposed to minimize this problem; first, a dynamic state graph pruning algorithm based on static analysis of the model structure to provide an exact minimization and second, approximation of the state graph with an estimation of the state space in a more compact representation. These techniques help delay the onset of state explosion, allowing useful information to be obtained and utilized, even for complex designs. Results and practical experiences of applying these techniques to the design of the node controller (MAGIC) of the Stanford FLASH Multiprocessor project are given.
http://i.stanford.edu/pub/cstr/reports/csl/tr/96/708/CSL-TR-96-708.pdf