Arithmetic Transforms of Imprecise Datapaths by Taylor Series Conversion

We develop a new method to compute representations of imprecise datapaths for purpose of equivalence checking and component matching. From a Taylor series, we devise an efficient algorithm to produce arithmetic transform (AT) which is a function representation behind word-level decision diagrams such as BMDs. Also, we introduce an efficient algorithm for verifying the imprecise circuits.