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

• URL: http://arxiv.org/abs/2405.01572v1
• Date: Sat, 20 Apr 2024 12:18:47 GMT
• Title: A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs
• Authors: Aman Kumar, Sebastian Simon,
• Abstract summary: A majority of System-on-Chips (SoCs) make use of Intellectual Property (IP) in order to shorten development cycles. The vast number of possibilities does not allow a brute-force approach. This paper is focused on a semi-formal verification methodology for efficient configuration coverage.
• Score: 2.655207969975261
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks. Digital and Analog Mixed-Signal (AMS) designs, which are fundamentally different in nature, are integrated seamlessly in a formal verification setup.
  arXiv  Detail & Related papers  (2024-09-23T13:38:31Z)
• Efficient Stimuli Generation using Reinforcement Learning in Design Verification [2.9652396326501864]
  Reinforcement Learning (RL) is proposed to generate efficient stimuli with the help of Reinforcement Learning (RL) to reach the maximum code coverage of the Design Under Verification (DUV) In this paper, a novel methodology is proposed to generate efficient stimuli with the help of Reinforcement Learning (RL) to reach the maximum code coverage of the Design Under Verification (DUV)
  arXiv  Detail & Related papers  (2024-05-30T08:23:04Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Near-optimal Policy Identification in Active Reinforcement Learning [84.27592560211909]
  AE-LSVI is a novel variant of the kernelized least-squares value RL (LSVI) algorithm that combines optimism with pessimism for active exploration. We show that AE-LSVI outperforms other algorithms in a variety of environments when robustness to the initial state is required.
  arXiv  Detail & Related papers  (2022-12-19T14:46:57Z)
• CPPF++: Uncertainty-Aware Sim2Real Object Pose Estimation by Vote Aggregation [67.12857074801731]
  We introduce a novel method, CPPF++, designed for sim-to-real pose estimation. To address the challenge posed by vote collision, we propose a novel approach that involves modeling the voting uncertainty. We incorporate several innovative modules, including noisy pair filtering, online alignment optimization, and a feature ensemble.
  arXiv  Detail & Related papers  (2022-11-24T03:27:00Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  This work proposes easy to interpret validation diagnostics for multi-dimensional conditional (posterior) density estimators based on NF. It also offers theoretical guarantees based on results of local consistency. This work should help the design of better specified models or drive the development of novel SBI-algorithms.
  arXiv  Detail & Related papers  (2022-11-17T15:48:06Z)
• Real-Time Scene Text Detection with Differentiable Binarization and Adaptive Scale Fusion [62.269219152425556]
  segmentation-based scene text detection methods have drawn extensive attention in the scene text detection field. We propose a Differentiable Binarization (DB) module that integrates the binarization process into a segmentation network. An efficient Adaptive Scale Fusion (ASF) module is proposed to improve the scale robustness by fusing features of different scales adaptively.
  arXiv  Detail & Related papers  (2022-02-21T15:30:14Z)
• Fingerprint recognition with embedded presentation attacks detection: are we ready? [6.0168714922994075]
  The diffusion of fingerprint verification systems for security applications makes it urgent to investigate the embedding of software-based presentation attack algorithms (PAD) into such systems. Current research did not state much about their effectiveness when embedded in fingerprint verification systems. This paper proposes a performance simulator based on the probabilistic modeling of the relationships among the Receiver Operating Characteristics (ROC) of the two individual systems when PAD and verification stages are implemented sequentially.
  arXiv  Detail & Related papers  (2021-10-20T13:53:16Z)
• Multi-Exit Semantic Segmentation Networks [78.44441236864057]
  We propose a framework for converting state-of-the-art segmentation models to MESS networks. specially trained CNNs that employ parametrised early exits along their depth to save during inference on easier samples. We co-optimise the number, placement and architecture of the attached segmentation heads, along with the exit policy, to adapt to the device capabilities and application-specific requirements.
  arXiv  Detail & Related papers  (2021-06-07T11:37:03Z)
• Multi-objective Optimisation of Digital Circuits based on Cell Mapping in an Industrial EDA Flow [0.2578242050187029]
  A fully-automated, multi-objective (MO) EDA flow is introduced to address this issue. We have applied the proposed MOEDA framework to ISCAS-85 and EPFL benchmark circuits using a commercial 65nm standard cell library.
  arXiv  Detail & Related papers  (2021-05-21T15:29:58Z)
• Offline Model-Based Optimization via Normalized Maximum Likelihood Estimation [101.22379613810881]
  We consider data-driven optimization problems where one must maximize a function given only queries at a fixed set of points. This problem setting emerges in many domains where function evaluation is a complex and expensive process. We propose a tractable approximation that allows us to scale our method to high-capacity neural network models.
  arXiv  Detail & Related papers  (2021-02-16T06:04:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.