2012 · 23 citations · 15 references
ComputingComputer EngineeringComputer ScienceDiagnostic ReasoningFault-tolerant ComputingFault-tolerant SystemsDesign For TestabilityDiagnosisDiagnosticsFault DetectionFault DiagnosisSatisfiability Modulo TheoriesAutomatic Test Pattern GenerationBoolean Satisfiability Modulo TheoriesCombinational Logic SynthesisDiagnostic Test GenerationHeuristicsSatisfiabilitySearch Space PruningTest Generation
A diagnostic test pattern generator using a Satisfiability Modulo Theory (SMT) solver is proposed. Rather than targeting a single fault pair at a time, the proposed SMT approach can distinguish multiple fault pairs in a single instance. Several heuristics are proposed to constrain the SMT formula to further reduce the search space, including fault selection, excitation constraint, reduced primary output vector, and cone-of-influence reduction. Experimental results for the ISCAS85 and full-scan versions of ISCAS89 benchmark circuits show that fewer diagnostic vectors are generated compared with conventional diagnostic test generation methods. Up to 73% reduction in the number of vectors generated can be achieved in large circuits.
15
Bounded Model Checking Using Satisfiability Solving
Edmund M. Clarke, Armin Biere, Richard Raimi et al. · Formal Methods in System Design · 2001 · 679 citations
Bruno Dutertre, Leonardo de Moura · 2006 · 483 citations
Test set compaction algorithms for combinational circuits
İlker Hamzaoğlu, J.H. Patel · 1998 · 432 citations · Full text