Abstract:

     In order to prove that the fixedpoint arithmetic specification is equivalence to the translated Register Transfer Level (RTL) implementation, the fixedpoint datapaths, which perform ADD, MULT and SHIFT operations, are modeled by combining arithmetic transform (AT) and polynomial function. According to the results of polynomial function, the upper bound of simulated vectors is obtained for the equivalence verification of the fixedpoint datapaths, which avoids the exhaustive simulation. Experiment results show that the proposed method is effective.

Key words: computersystemarchitecture, equivalence verification, datapaths, polynomialfunction, arithmetictransforms