In this paper, we outline the use of a special kind of polynomial expressions in specifying and verifying arithmetic circuits found in modern DSP systems. It is shown that there exists a compact canonical representation of a class of arithmetic circuits under various number encoding schemes. Compared to some recent decision-diagram based representations, this form is canonical. Component matching of circuits such as adders and multipliers can be done in linear time. Verification time can be shortened under assumption of corrupting a bounded number of polynomial coefficients. Bounds are derived for such verifications.