Paper Title :Recent Developments In VBMC: A Formal Verification Tool For HDL Designs

Author :Asha Devi, Ajith K John, R. Dhanabal

Article Citation :Asha Devi ,Ajith K John ,R. Dhanabal , (2016 ) " Recent Developments In VBMC: A Formal Verification Tool For HDL Designs " , International Journal of Electrical, Electronics and Data Communication (IJEEDC) , pp. 32-35, Volume-4,Issue-6

Abstract : Verification is inevitable in order to make hardware designs reliable and bug free. The conventional method for hardware design verification involves simulation and testing. However, exhaustive testing and simulation over the entire behavior space of the design is infeasible even for designs of moderate size and complexity. Formal verification provides a feasible alternative for verification of hardware designs. Given a hardware design and functional property, a formal verification tool either proves that the design satisfies the property or generates an execution of the design violating the property. Application of such tools is highly recommended in hardware designs used in safety critical applications such as nuclear reactors. VHDL Bounded Model Checker (VBMC) is a formal verification tool for VHDL designs developed in-house at BARC. VBMC accepts a VHDL design, a functional property, and verification bound (number of cycles of operation) as inputs. It either reports that the design satisfies the functional property for the given verification bound or generates a counterexample providing the reason of violation. In case of satisfaction, the proof holds good for the verification bound. This paper presents the overview of the tool VBMC with focus on its recent developments. Keywords- Preprocessor, Property Translator, VHDL,VBMC

Type : Research paper

Published : Volume-4,Issue-6

	|		PDF	|	Viewed - 92	|	Published on 2016-07-02