Using SAT for verification in the presence of unknowns

In order to debug IP-based designs in early stages, people often need to verify partial implementation. In this paper, an efficient approach based on Boolean satisfiability (SAT) for verification in the presence of unknowns is presented. We use universally quantified conjunctive normal form (CNF) formula to represent the miter network with unknown constraints, our method achieves higher performance gains, and obtains one to three orders of magnitude performance improvement on ISCAS 85 benchmark circuits than other previous methods.