I. Introduction
Effort for verification of digital system designs grows as their size and complexity increase. In many practical designs such as Digital Signal Processing (DSP) for multimedia applications, arithmetic circuits are the main part of their datapaths. So verification of arithmetic circuits in a fast and precise way plays an important role in a digital system design flow. Several methods have been proposed to check an arithmetic circuit against its specification at a higher level of abstraction. Most of them are based on canonical graph-based representations like Binary Decision Diagrams (BDDs) that are not scalable because they suffer from space and time explosion problems when dealing with large arithmetic circuits especially multipliers [16] [17].