1. A computer program product embodied on a tangible 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, where the transforming normalizes at least some of the plurality of finite portions and extracts a word-level intent of the netlist; 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; and computer code for performing an abstraction on the netlist, where performing the abstraction includes one or more of replacing predetermined types of operators in the netlist and removing a control portion of the netlist; wherein the plurality of infinite portions include 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; wherein the plurality of infinite portions include one or more of lossless regions of the netlist and at least one infinite operator; wherein the plurality of finite portions include one or more of lossy regions of the netlist and at least one finite operator.