Hierarchical Design Verification and Error Diagnosis Using Boolean Satisfiability

In this paper, we present a novel technique integrating logic simulation and Boolean satisfiablity (SAT) for verifying the designs with black boxes, and generalize this technique to improve the accuracy of design error diagnosis. This technique uses intelligent set of vectors instead of randomly generated vectors for logic simulation during black box equivalence checking and error diagnosis process. In addition, the SAT-based technique can avoid the potential memory explosion which binary decision diagram (BDD) based approaches often suffer from, and can enhance the simulation-based validation efficiently. Experimental results on ISCAS´85 benchmark circuits show the efficiency of the presented technique.