Residue BDD and its application to the verification of arithmetic circuits
Shinji Kimura · 1995
The paper describes a veri cation method for arithmetic circuits based on residue arithmetic.In the veri cation, a residue module is attached to the speci cation and the implementation, and these outputs are compared by constructing BDD's.For the BDD construction without node explosion, we i n troduce a residue BDD whose width is less than or equal to a modulus.The method is useful for multipliers including C6288.