Formal Verification under Unknown constraints

摘要

We prcstm a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT ). This method is based on a new encoding scheme of unknown constraints- and solves the corresponding conjunctivc normal form(CNF) formulas Furthermore, this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs, Experimental results demonstrate the efficiency and feasibility of the proposed method.