A dynamic specification to automatically debug and correct various divider circuits |
| |
| Affiliation: | 1. Jaypee University of Engineering and Technology, Raghogarh, Madhya Pradesh, India;2. School of Computer Engineering, Nanyang Technological University, Nanyang Avenue, Singapore 639798, Singapore;3. Department of Electrical and Computer Engineering, Concordia University, Montreal, QC, Canada H3G 2W1;1. Department of Industrial Engineering (D.I.In.), University of Salerno, Fisciano, Salerno, Italy;2. Advanced System Technology-STMicroelectronics International N.V., Plan-les-Quates, Switzerland;3. Advanced System Technology-STMICROELECTRONICS, Agrate Brianza, Milano, Italy;1. iPack Vinn Excellence Center, School of Information and Communication Technology, Royal Institute of Technology (KTH) Electrum 229, 164 40 Stockholm-Kista, Sweden;2. School of Information Science and Technology, Fudan University, Shanghai, China;1. Université de Saad Dahleb, Route de Soumaa, BP 270 BLIDA, Ouled Yaich 09200, Algeria;2. Centre de Développement des Energies Renouvelables, CDER, BP 62 Route de l’Observatoire, Bouzaréah 16340, Algiers, Algeria;1. School of Electrical Engineering, KAIST, Daejeon 305-701, Korea;2. Synopsys Inc., Mountain View, CA 94043, USA;3. School of Electrical and Computer Engineering, UNIST, Ulsan 689-798, Korea |
| |
| Abstract: | 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. |
| |
| Keywords: | Arithmetic and logic units Debugging aids Diagnostics Verification Formal models |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
