Multiple Design Error Diagnosis Using Boolean Satisfiability

A novel design error diagnosis algorithm for combinational circuits is presented.It can perform model-free logic error location by combining traditional simulation-based approach with a SAT solver.An incremental SAT-based diagnosis method is proposed.We improved the resolution and accuracy of diagnosis by ranking and screening sat solutions with structural information of circuits.A number of heuristics are proposed that keep the method's memory and run-time efficient.Experimental results show that using formal techniques to direct simulation captures the main characteristics of error location and improves the effectiveness and efficiency of design error diagnosis.