Formal Verification Methodology in an Industrial Setup

This paper presents a practical methodology for applying formal verification on industrial designs. The methodology is developed considering the quality, efficiency and productivity required in an industrial verification setup. The flow proposes a systematic approach addressing various aspects of the formal verification. First, the design implementation (RTL) is analyzed for its formal friendliness based on several predefined criteria. Next, a property automation flow is adapted for an efficient property development. Later, a series of verification tasks, grouped into formal test plan and formal execution plan are carried out to reach the formal sign-off stage. To demonstrate the applicability and effectiveness of the methodology, the proposed flow has been successfully applied on several industrial designs. In this paper, we consider the formal verification of Error Correction Codes, generally implemented in program and data flash memory interfaces to benchmark the proposed flow. Automatic property generation flow is used to generate an optimal property set with varying abstraction levels. The property proof runtimes are drastically reduced and better coverage compared to the previous hand-written properties has been achieved. New RTL bugs and specification errors have been found that were previously missed during the simulation.