This research addresses computation of reachable states for VLSI designs described in high-level languages and the application of these results to automatic test pattern generation (ATPG). Methods to compute symbolically the set of states reachable from an initial state are being explored. An extended finite state machine (ESFM) model, which can represent communication protocols and hardware behavior, is being used. A key idea is that the model allows use of arbitrary state variables, such as boolean and arithmetic, which will provide efficiency in computation. Methods and prototype tools to convert automatically a design in VHDL to an ESFM are being developed. These methods and techniques are being applied to ATPG for sequential circuit test.
