Using arithmetic transform for verification of datapath circuits via error modeling

In this paper, we consider verification under error-model assumption. We exploit the algebraic properties of the arithmetic transforms that are used in compact graph-based representations of arithmetic circuits, such as *BMDs. Verification time can be shortened under the assumption of corrupting a bounded number of transform coefficients. Bounds are derived for a number of test vectors, and the vectors successfully verified arithmetic circuits under a class of error models derived from recently proposed basic design error classes, including single stuck-at faults