Ajith K. John

Assertion Based Verification is a design methodology that integrates Formal Methods as part of the design process. As each module is designed, the designer expresses the functional, structural and interface requirements of the module as logical formulas called assertions. These assertions are then verified using simulation and/or formal verification. This paper aims at studying the effectiveness of applying formal verification during Assertion Based Verification in the development of VHDL design for a VME-bus for safety applications in nuclear reactors. Assertions for the VHDL modules developed were expressed in PSL, and were proved using three industrially successful and popular formal verification algorithms – Bounded Model Checking, K-Induction, and Property Driven Reachability, implemented in an open-source verification tool, Yosys. Our experiments revealed that Property Driven Reachability completely outperforms K-Induction in all the cases. Bounded Model Checking for a few hundred clock cycles helped us in finding a number of important, but subtle bugs, which were missed by traditional simulation, at the cost of a justifiable increase in design effort towards writing assertions.

FPGA-based intelligent hardware modules are increasingly being used in safety systems of nuclear power plants. Qualification of these modules as per safety standards such as IEC 62566/60880 and IEEE-7.4.3.2-2010 needs considerable effort. Many of the safety standards demand high rigour in verifying that designs of these modules meet the design intent. Use of Hardware Description Languages such as VHDL or Verilog makes the process of code review and verification difficult due to the complex non-sequential semantics of these languages. It is now recognized that formal verification offers a complementary approach to conventional verification. Formal verification tools perform analysis of designs based on language semantics to prove/refute their functional correctness. In this paper, we present the architecture of a formal verification tool for VHDL designs, and our experience of using this tool on VHDL designs in nuclear applications.