Satisfiability based test generation for stuck-at fault coverage in RTL circuits using VHDL

Due to the increasing complexity of modern circuit design, verification has become the major bottleneck of the entire design process. Most efforts are to verify the correctness of the initial Register-Transfer Level (RTL) descriptions written in Hardware Description Language (HDL). A digital system, in general, consists of two main parts: a data path and controller. A validation test set is used to verify controller behaviour and, the controller behaviour exercised by test sequences in a validation test set are reused for detecting faults in the data path. Such controller behaviours are said to be compatible with the corresponding pre-computed test vectors/responses, resulting in the detection of a majority of stuck-at faults in the data path RTL modules. Also, since test generation is performed at the RTL and the controller behaviour is predetermined, test generation time is reduced. The Justification algorithm is used to quickly identify whether the controller behaviour is compatible with pre-computed test pattern and it is a basic factor in affecting the efficiency of algorithms for test generation. Adding Design For Testability (DFT) elements is equivalent to modifying these clauses, such that all the unsatisfiable segment becomes satisfiable. A greedy algorithm is used to select circuit variables for DFT and minimizes the number of DFT elements added to a circuit.