SAT-Based Fault Equivalence Checking in Functional Safety Verification

Detecting equivalence classes of injected faults for functional verification of electronic systems is an important task because it helps reducing the number of faults to qualify a verification environment, and hence, improves the performance of qualification process and the validation time required for large-scale electronic systems. This paper describes an efficient way of detecting equivalent injected faults in a mapped netlist in order to speedup the qualification process of a verification environment for functional safety. The presented fault models include general faults resulting in arbitrary functional changes, in addition to conventional stuck-at faults. The solution is based on structural pruning and functional analysis performed by a synergistic combination of iterative Boolean satisfiability and guided simulation. It should be noted that traditional brute-force-like methods would take many hours or even days to identify thousands of equivalent functional faults injected to a small circuit with only hundred of cells. The proposed approach can achieve excellent fault reduction ratios within few seconds for such small circuits. The implementation also scales well for the largest ISCAS'89 and OpenCores benchmarks containing over 35K gates and 490K general functional faults.