Design and Application of a Formal Verification Tool for VHDL Designs

摘要

The design of Control and Instrumentation (C & I) systems used in safety critical applications such as nuclear power plants involves partitioning of the overall system functionality into subparts and implementing each subpart in hardware and/or software as appropriate. With increasing use of programmable devices like FPGA, the hardware subsystems are often implemented in Hardware Description Languages (HDL) like VHDL. Since the functional bugs in such hardware subsystems used in safety critical C&l systems have disastrous consequences, it is important to use rigorous reasoning to verify the functionalities of the HDL models. We describe our work on developing a software tool named VBMC (VHDL Bounded Model Checker) for mathematically proving functional properties of hardware designs described in VHDL. It is based on the principle of bounded model checking. Although the design of VBMC is still evolving, it is currently also being used for the functional verification of FPGA based intelligent I/O (EHS) boards developed in Reactor Control Division, BARC.