Register-transfer-level functional verification techniques

As the scale of the VLSI circuits grows into multi-million gates per chip, functional verification has become the largest bottleneck in the design process. In general, functional verification can be viewed as translating the high-level specification into temporal properties and using verification tools to validate the corresponding constraints of these properties. Traditional verification approaches like simulation and symbolic model checking are either suffered from the incompleteness in algorithms, limitation in capacity, difficulty in usage, or deficiency in performance.; In this thesis, we propose a word-level Automatic Test Pattern Generation (ATPG) technique based on a new Extended Finite State Machine (EFSM) model to verify the assertion and witness properties for modern industrial designs. There are four major components in our framework: (1) an interface to a commercial Hardware Description Language (HDL) parser/logic synthesizer to transform the industrial designs into our internal data structures, (2) a word-level logic implication routine to derive the implications for both controller and datapath circuits and translate the learned information from one to the other, (3) an advanced Boolean justification technique which contains a novel dynamic decision variable reordering algorithm to solve the constraints in the controller circuit, and (4) an arithmetic constraint solver based on the modular number system to analyze the constraints in the datapath circuit.; We have implemented the word-level ATPG algorithms as a framework and tested it on several benchmark and industrial designs. The experimental results show that our approach is very efficient in both runtime and memory usage, and is applicable to a broad class of designs. With this powerful constraint-solving engine, our RTL functional verification framework can also be used as the basis for many future research topics.