RTL Test Generation via Fault Insertion and Hybrid Satisfiability Solving
Weimin Wu · 2008
Test generation at RTL (Register-Transfer Level) is a challenging task because bit and word variables co-existent and the high-level functional units impose more complex constraints.We propose an effective way to the problem.In our method, given the circuit as well as the fault point to be checked, we first construct a new circuit, miter, by fault insertion as well as miter reduction techniques.Then we solve the constraints of the miter by EHSAT, an efficient hybrid satisfiability solver to obtain the required test vectors.Experimental results demonstrate the effectiveness of our method.