Analogous Alignments: Digital "Formally" meets Analog

• URL: http://arxiv.org/abs/2409.15013v1
• Date: Mon, 23 Sep 2024 13:38:31 GMT
• Title: Analogous Alignments: Digital "Formally" meets Analog
• Authors: Hansa Mohanty, Deepak Narayan Gadde,
• Abstract summary: 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The complexity of modern-day System-on-Chips (SoCs) is continually increasing, and it becomes increasingly challenging to deliver dependable and credible chips in a short time-to-market. Especially, in the case of test chips, where the aim is to study the feasibility of the design, time is a crucial factor. Pre-silicon functional verification is one of the main contributors that makes up a large portion of the product development cycle. Verification engineers often loosely verify test chips that turn out to be non-functional on the silicon, ultimately resulting in expensive re-spins. To left-shift the verification efforts, formal verification is a powerful methodology that aims to exhaustively verify designs, giving better confidence in the overall quality. This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks. This paper discusses a novel approach of including the analog behavioral model into the formal verification setup. Digital and Analog Mixed-Signal (AMS) designs, which are fundamentally different in nature, are integrated seamlessly in a formal verification setup, a concept that can be referred to as "Analogous Alignments". Our formal setup leverages powerful formal techniques such as FPV, CSR verification, and connectivity checks. The properties used for FPV are auto-generated using a metamodeling framework. The paper also discusses the challenges faced especially related to state-space explosion, non-compatibility of formal with AMS models, and techniques to mitigate them such as k-induction. With this verification approach, we were able to exhaustively verify the design within a reasonable time and with sufficient coverage. We also reported several bugs at an early stage, making the complete design verification process iterative and effective.

Related papers

• Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
  We propose an automated methodology based on metamodeling techniques which consist of two main steps. First, an untimed algorithmic description written in C++ is verified in an early stage using generated assertions. Second, this algorithmic description is verified against its sequential design using HLEC and the respective metamodel parameters.
  arXiv  Detail & Related papers  (2024-10-24T06:09:40Z)
• Pragmatic Formal Verification Methodology for Clock Domain Crossing (CDC) [2.3624953088402734]
  This paper focuses on the development of a pragmatic formal verification methodology to minimize the Clock Domain Crossings (CDC) issues. CDCs are prone to metastability effects and functional verification of such CDC is very important to ensure that no bug escapes.
  arXiv  Detail & Related papers  (2024-04-20T13:17:25Z)
• A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs [2.655207969975261]
  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.
  arXiv  Detail & Related papers  (2024-04-20T12:18:47Z)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity. We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
  arXiv  Detail & Related papers  (2023-12-13T21:53:32Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  Hardware-firmware co-verification is critical to design trustworthy systems. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification.
  arXiv  Detail & Related papers  (2023-09-14T19:24:57Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Improving Text Matching in E-Commerce Search with A Rationalizable, Intervenable and Fast Entity-Based Relevance Model [78.80174696043021]
  We propose a novel model called the Entity-Based Relevance Model (EBRM) The decomposition allows us to use a Cross-encoder QE relevance module for high accuracy. We also show that pretraining the QE module with auto-generated QE data from user logs can further improve the overall performance.
  arXiv  Detail & Related papers  (2023-07-01T15:44:53Z)
• Precision-Recall Divergence Optimization for Generative Modeling with GANs and Normalizing Flows [54.050498411883495]
  We develop a novel training method for generative models, such as Generative Adversarial Networks and Normalizing Flows. We show that achieving a specified precision-recall trade-off corresponds to minimizing a unique $f$-divergence from a family we call the textitPR-divergences. Our approach improves the performance of existing state-of-the-art models like BigGAN in terms of either precision or recall when tested on datasets such as ImageNet.
  arXiv  Detail & Related papers  (2023-05-30T10:07:17Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems [20.491263196235376]
  We focus on learning-enabled state estimation systems (LE-SESs), which have been widely used in robotics applications. We study LE-SESs from the perspective of formal verification, which determines the satisfiabilty of a system model.
  arXiv  Detail & Related papers  (2020-10-16T11:06:50Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) The approach is underpinned by an inductive framework, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples. The outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine.
  arXiv  Detail & Related papers  (2020-07-07T07:39:42Z)

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.