FVM: A Formal Verification Methodology for VHDL Designs

With the increasing complexity of digital designs, functional verification is becoming unmanageable. Bugs that survive verification cause a number of issues with functional, performance, security, safety and economic impact, and are unfortunately prevalent in current FPGA and ASIC designs, manifesting in later stages of development or even after the design has been deployed or manufactured. In this context, Formal Verification poses itself as a powerful complement to verification by simulation, which is currently the most extended verification method. By mathematically proving properties of the designs, Formal Verification allows to verify them with high confidence, but also requires designers to have deep expertise of the methods, techniques and tools. Thus, adoption of formal methods for verification is not as extended as their usefulness may suggest, and even less in the case of VHDL teams. To lower the adoption barriers for formal verification of digital designs, the present paper proposes a Formal Verification Methodology, which is complemented by a build and test framework and a repository of examples. Results of applying the Formal Verification Methodology to the repository of examples show compelling results both in manageable design complexity and verification productivity.