Verifying Imprecisely Working Arithmetic Circuits

If real number calculations are implemented as circuits, only a limited preciseness can be obtained. Hence, formal verification can not be used to prove the equivalence be-tween the mathematical specification based on real num-bers and the corresponding hardware realization. Instead, the number representation has to be taken into account in that certain error bounds have to be verified. For this reason, we propose formal methods to guide the complete design flow of these circuits from the highest ab-straction level down to the register-transfer level with for-mal verification techniques that are appropriate for the cor-responding level. Hence, our method is hybrid in the sense that it combines different state-of-the-art verification tech-niques. Using our method, we establish a more detailed no-tion of correctness that considers beneath the control and data flow also the preciseness of the numeric calculations. We illustrate the method with the discrete cosine transform as a real-world example. 1