Patent ID: 8640065

Claim:
A method comprising: receiving, by using a computer, a first description for a circuit whose operation over a plurality of inputs is to be verified; receiving, by using the computer, a second description for expected behavior of the circuit, where the expected behavior in the second description is expressed as at least one expected value under a set of algebraic systems of multivariable polynomials over at least one Galois field; applying at least one computational algebraic geometry technique to a combination of the first description and the second description; adjusting a time limit for the at least one computational algebraic geometry technique to increase a number of attempts of the at least one computational algebraic geometry technique to determine whether the circuit is verified, confirming that at least one output obtained based on the first description corresponds to at least one expected value based on the expected behavior expressed in the second description; outputting, by using the computer, an indication as to whether the circuit is verified; and where applying the at least one computational algebraic geometry technique further comprises, in response to encountering a Boolean satisfiability that cannot be resolved, forking to at least two branches that continue independently based on at least two different assumptions.