Patent ID: 7302656
Filing Date: 2007-11-27
Classification: G06F

Abstract:
1. A computer-implemented method comprising: providing a first netlist, wherein a subset of the first netlist includes a plurality of inputs and a plurality of outputs and wherein the subset is an arithmetic circuit; modifying the first netlist to obtain a second netlist by replacing the subset with a random value generator and associating the random value generator with the outputs such that the random value generator supplies random values to the outputs; identifying a testing counterexample using the second netlist, wherein the testing counterexample is associated with particular values of the outputs; generating, for the inputs of the subset, a set of input values corresponding to said particular values of the outputs such that the input values represent operands to an arithmetic operation and said particular values of the outputs represent a result of the arithmetic operation; and verifying the first netlist using the generated set of input values.