Effective Application of Formal Verification Techniques for VLSI Digital Design Verification

Abstract

The design of CMOS Digital Integrated Circuits (ICs) is becoming increasingly complicated, making it challenging to achieve design verification objectives like code or functional coverage closure. These difficulties result in endless design verification time and effort for every digital design. The main issue with design verification that modern silicon designs on formal verification platforms and simulation/stimulation-driven platforms encounter is Functional Verification signoff towards Silicon Tape-Out. Currently, functional verification signoff on RTL digital designs relies on CAD/EDA tools in conjunction with random seed capability of constrained random verification approaches like Universal Verification Methodology (UVM) and Formal Verification Methodology (FVM) based on mathematical proofing procedures. A custom-specific criterion known as Formal Verification Convergence is based on the verification objectives developed and certified by the Formal Tool, and it considers their success or failure as well as their exhaustiveness and reachability. The ability to mathematically demonstrate the equivalency between two distinct versions of the same RTL Designs is fundamental in Formal Verification. This paper will analyze the formal verification techniques suited for effective deployment on VLSI digital designs towards formal verification convergence, guaranteeing bug-free silicon tape-outs. Specifically, we will explore the 'equivalence checking' and 'feature checking' capabilities of Formal Verification Methodology (FVM) using IEEE 1800^TM System Verilog Assertions.