Formal Verification Methodology in an Industrial Setup

Lorenzo Servadei, Zhao Han, Michael Werner, Wolfgang Ecker, Keerthikumara Devarajegowda

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

8 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - Euromicro Conference on Digital System Design, DSD 2019
EditorsNikos Konofaos, Paris Kitsos
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages610-614
Number of pages5
ISBN (Electronic)9781728128610
DOIs
StatePublished - Aug 2019
Event22nd Euromicro Conference on Digital System Design, DSD 2019 - Kallithea, Chalkidiki, Greece
Duration: 28 Aug 201930 Aug 2019

Publication series

NameProceedings - Euromicro Conference on Digital System Design, DSD 2019

Conference

Conference22nd Euromicro Conference on Digital System Design, DSD 2019
Country/TerritoryGreece
CityKallithea, Chalkidiki
Period28/08/1930/08/19

Keywords

  • Formal Verification
  • Model Driven Property Generation

Fingerprint

Dive into the research topics of 'Formal Verification Methodology in an Industrial Setup'. Together they form a unique fingerprint.

Cite this