Recent Developments In VBMC: A Formal Verification Tool For HDL Designs
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
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