Patent ID: 7418369

Claim:
A method implemented at least in part by a machine for determining satisfying variable assignments of a Boolean formula, or for determining that no satisfying variable assignments exist, to find an error in or prove the design correctness of a software program or a hardware circuit, the method comprising the steps of: a. generating a Boolean formula representing error conditions of the software program or the hardware circuit; b. assigning an unassigned variable in the Boolean formula to zero or one; c. generating implications in the Boolean formula resulting from the assignment using Boolean Constraint Propagation, wherein implications are generated by watching two literals within a sub-formula corresponding to a clause or a gate in the Boolean formula, the two literals watched being randomly selected from literals not assigned to zero; and d. continuing steps (b) and (c) until reaching a conflict or until all variables are assigned, wherein upon reaching a conflict the assignment of at least one variable is changed, implications resulting from the changed assignment are generated and steps (b) and (c) continue until determining a satisfying variable assignment, whereby the software program or the hardware circuit is proved incorrect, with the satisfying variable assignment representing the incorrectness condition, or until determining that no satisfying variable assignment exists, whereby the software program or the hardware circuit is proved correct.