A dynamic specification to automatically debug and correct various divider circuits

This paper presents a formal technique to verify and debug division circuits on fixed point numbers. The proposed technique is based on a reverse-engineering mechanism of obtaining a high level model of the gate level implementation and also introducing an intermediate representation of the specification that makes equivalence checking between two models possible. The main advantage of this representation is the fact that the specification is dynamically updated according to the information obtained from the implementation. At the end, if two updated models are not equivalent, possible bugs can be localized and then corrected automatically by analyzing the difference, if possible. Experimental results show the robustness of the proposed technique in comparison with other contemporary methods in terms of the run time and also show that two orders of magnitude average speedup is obtained.