SAT-Based fault equivalence checking in functional safety verification

Ai Quoc Dao, Po-Hung Lin*, Alan Mishchenko

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Scopus citations


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.

Original languageEnglish
Article number8252779
Pages (from-to)3198-3205
Number of pages8
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number12
StatePublished - 1 Dec 2018


  • Equivalence checking
  • equivalence classes
  • equivalent fault
  • fault collapsing
  • fault injection
  • fault reduction
  • functional safety
  • functional verification
  • general fault
  • identical fault
  • ISO 26262
  • qualification acceleration
  • stuck-at fault


Dive into the research topics of 'SAT-Based fault equivalence checking in functional safety verification'. Together they form a unique fingerprint.

Cite this