Patent Document ID: 7730436
Application ID: 11554169
Patent Flag: 1

Claim One:
1. A method for performing design verification of a system, the method comprising: receiving a formula comprising a set of clauses, each clause comprising a disjunction of literals; receiving a plurality of proof objective literals, each proof objective literal comprising a variable or a negation of the variable, wherein the variable or the negation of the variable occurs in the formula; performing operations on a satisfiability search space until no unresolved proof objective literal exists, the operations comprising: assigning an unresolved proof objective literal of the plurality of proof objective literals as a currently watched proof objective literal; performing Boolean constraint propagation on the formula; if a model is found during the Boolean constraint propagation, designating proof objective literals that are assigned false by the model as falsifiable and un-assigning literals of the formula that are not globally true; and designating globally true proof objective literals as valid proof objective literals; wherein the above steps of the method are executed by a processor-based system to perform the system design verification.