HDL slicing for verification and test

Abstract

The semiconductor industry has been increasingly relying on computer-aided design (CAD) tools in order to meet its demand for high performance and stringent time-to-market requirements. However, practical application of state-of-the-art CAD tools is severely limited by the sheer size of the design sizes. Therefore, an appropriate methodology that exploits the inherent modular structure within the complex designs, is desired. This dissertation proposes such a methodology that is useful with a variety of CAD tools in design verification and manufacturing test generation. Functional test generation using sequential automatic test pattern generation (ATPG) tools is extremely computation intensive and produces acceptable results only on relatively small designs. Therefore, hierarchical approaches are necessary to reduce the ATPG complexity. A promising approach was previously proposed in which individual modules in a design are targeted one at a time, using an ad-hoc abstraction for the reminder of the design derived from its register-transfer level (RTL) model. Based on this approach, an elegant and a systematic approach based on “program slicing”, that allows it to be scalable for large designs, is developed. The theoretical basis for applying program slicing on hardware description languages (HDLs) is established, and a tool called FACTOR has been implemented to automate the approach for test generation and testability analysis. Design verification requires exploring the complete design space to ensure the correctness of the design. A proof-by-contradiction approach called bounded model checking (BMC) has been proposed, which utilizes satisfiability (SAT) capabilities to find counterexamples for temporal properties within a specified number of time steps. The proposed scheme harnesses the power of sequential-ATPG tools to use structural information of a hardware design, to perform BMC more efficiently. This approach has been further augmented by the HDL slicing methodology for test generation, to accelerate the verification methodology. Symbolic simulation uses symbols rather than actual values for simulating a hardware design, so that the responses to a class of values can be computed and checked for correctness in a single run. The effectiveness of this approach has been incorporated into a powerful verification methodology, called symbolic trajectory evaluation (STE), to verify properties of bounded state sequences, intermixed with properties of invariant behavior. Assertions are described in a limited form of temporal logic and are symbolically validated against the design under verification. The HDL slicing tool, FACTOR, has been appropriately applied to speed up the verification of the floating point adder-subtractor unit of the Pentium 4 design in Intel’s Forte verification framework.