Formal Verification Methodology in an Industrial Setup
| Autor: | Michael Werner, Zhao Han, Lorenzo Servadei, Wolfgang Ecker, Keerthikumara Devarajegowda |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Computer science
Property (programming) business.industry 02 engineering and technology Automation 020202 computer hardware & architecture Reliability engineering Set (abstract data type) 0202 electrical engineering electronic engineering information engineering Benchmark (computing) 020201 artificial intelligence & image processing Test plan Error detection and correction business Formal verification Abstraction (linguistics) |
| Zdroj: | DSD |
| DOI: | 10.1109/dsd.2019.00094 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|