Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs

Aman Kumar, Sebastian Simon

TL;DR

The paper tackles the challenge of verifying highly configurable digital designs under ISO 26262, where exhaustive testing is infeasible. It introduces ConfigVerMet, a semi-formal workflow that combines vPlan-driven regression planning, Pairwise testing, Equivalence Class Verification, and Formal Structural Checking to reduce configuration space while preserving coverage. The approach is demonstrated on a SEooC microprocessor IP, achieving 17 optimized regressions and about 3.5 days runtime, and uncovering nine bugs, including testbench and RTL issues. The work provides automated artifacts for configuration coverage and shows scalability and safety-compliant verification for industrial IPs.

Abstract

Nowadays, a majority of System-on-Chips (SoCs) make use of Intellectual Property (IP) in order to shorten development cycles. When such IPs are developed, one of the main focuses lies in the high configurability of the design. This flexibility on the design side introduces the challenge of covering a huge state space of IP configurations on the verification side to ensure the functional correctness under every possible parameter setting. The vast number of possibilities does not allow a brute-force approach, and therefore, only a selected number of settings based on typical and extreme assumptions are usually verified. Especially in automotive applications, which need to follow the ISO 26262 functional safety standard, the requirement of covering all significant variants needs to be fulfilled in any case. State-of-the-Art existing verification techniques such as simulation-based verification and formal verification have challenges such as time-space explosion and state-space explosion respectively and therefore, lack behind in verifying highly configurable digital designs efficiently. This paper is focused on a semi-formal verification methodology for efficient configuration coverage of highly configurable digital designs. The methodology focuses on reduced runtime based on simulative and formal methods that allow high configuration coverage. The paper also presents the results when the developed methodology was applied on a highly configurable microprocessor IP and discusses the gained benefits.

A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs

TL;DR

The paper tackles the challenge of verifying highly configurable digital designs under ISO 26262, where exhaustive testing is infeasible. It introduces ConfigVerMet, a semi-formal workflow that combines vPlan-driven regression planning, Pairwise testing, Equivalence Class Verification, and Formal Structural Checking to reduce configuration space while preserving coverage. The approach is demonstrated on a SEooC microprocessor IP, achieving 17 optimized regressions and about 3.5 days runtime, and uncovering nine bugs, including testbench and RTL issues. The work provides automated artifacts for configuration coverage and shows scalability and safety-compliant verification for industrial IPs.

Abstract

Nowadays, a majority of System-on-Chips (SoCs) make use of Intellectual Property (IP) in order to shorten development cycles. When such IPs are developed, one of the main focuses lies in the high configurability of the design. This flexibility on the design side introduces the challenge of covering a huge state space of IP configurations on the verification side to ensure the functional correctness under every possible parameter setting. The vast number of possibilities does not allow a brute-force approach, and therefore, only a selected number of settings based on typical and extreme assumptions are usually verified. Especially in automotive applications, which need to follow the ISO 26262 functional safety standard, the requirement of covering all significant variants needs to be fulfilled in any case. State-of-the-Art existing verification techniques such as simulation-based verification and formal verification have challenges such as time-space explosion and state-space explosion respectively and therefore, lack behind in verifying highly configurable digital designs efficiently. This paper is focused on a semi-formal verification methodology for efficient configuration coverage of highly configurable digital designs. The methodology focuses on reduced runtime based on simulative and formal methods that allow high configuration coverage. The paper also presents the results when the developed methodology was applied on a highly configurable microprocessor IP and discusses the gained benefits.
Paper Structure (27 sections, 2 equations, 23 figures, 3 tables)

This paper contains 27 sections, 2 equations, 23 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Highly Configurable Digital Design
  4. Safety Element out of Context
  5. Simulation-Based Verification
  6. Formal Verification
  7. Semi-Formal Configuration Verification Methodology
  8. Overview of the Methodology
  9. Regression Plan Generation
  10. ConfigVerMet: Prepare
  11. Pairwise Verification
  12. ConfigVerMet: Extract
  13. Constraints
  14. Equivalence Class Verification
  15. Weak Normal Equivalence Class Verification
  16. ...and 12 more sections

Figures (23)

  • Figure 1: Verification efforts required in overall product development VerStudy
  • Figure 2: Relationship between assumptions and SEooC development iso
  • Figure 3: Formal verifier
  • Figure 4: Overview of the methodology
  • Figure 5: Regression plan generation flow
  • ...and 18 more figures