Residue BDD and Its Application to the Verification of Arithmetic Circuits

The paper describes a verification method for arithmetic circuits based on residue arithmetic. In the verification, a residue module is attached to the specification and the implementation, and these outputs are compared by constructing BDD´s. For the BDD construction without node explosion, we introduce a residue BDD whose width is less than or equal to a modulus. The method is useful for multipliers including C6288.