Formal Verification and Debugging of Array Dividers with Auto-correction Mechanism

Arithmetic circuits require a verification process to prove that the gate level circuit is functionally equivalent to a high level specification or not. Furthermore, if two models are not equivalent, we need to automatically localize bugs and correct them with minimum user intervention. This paper presents a formal technique to verify and debug arithmetic systems including dividers. The proposed technique is based on a reverse-engineering mechanism of obtaining a high level model of the gate level implementation and also presenting the specification at a lower level of abstraction which makes the equivalence checking between two models possible. During this process, if two high level models are not equivalent, possible bugs can be localized and then corrected automatically if possible. We have applied our technique to a wide range of arithmetic circuits including dividers, multipliers and their combinations. Preliminary experimental results show robustness of the proposed technique in comparison with other contemporary methods in terms of the run time. In average, two orders of magnitude average speedup is obtained.