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
DOIONLINE NO - IJEEDC-IRAJ-DOIONLINE-4748
View Here
Copyright: © Institute of Research and Journals
|
|
| |
|
PDF |
| |
Viewed - 92 |
| |
Published on 2016-07-02 |
|