Patent ID: 8122401

Claim:
A computer program product embodied on a non-transitory computer readable medium, comprising: computer code for identifying a netlist including a plurality of infinite portions and a plurality of finite portions; computer code for transforming at least some of the plurality of finite portions, utilizing at least one predetermined transformation; and computer code for determining an equivalence of the netlist and another netlist, utilizing at least a subset of the finite portions and the infinite portions; wherein the transformation identifies a word-level functionality of the at least some of the finite portions by converting bit-level functionality into word-level functionality; wherein the plurality of infinite portions of the netlist that are reasoned in infinite precision, such that unbounded integers are utilized for determining an equivalence of the infinite portions with other infinite portions of the other netlist; wherein the plurality of finite portions include portions of the netlist that are reasoned in finite precision, such that finite precision arithmetic is utilized for determining an equivalence of the finite portions with other finite portions of the other netlist.