论文部分内容阅读
We present 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 conjunctive normal form (