Pragmatic Formal Verification of Sequential Error Detection and Correction Codes (ECCs) used in Safety-Critical Design

• URL: http://arxiv.org/abs/2404.18270v1
• Date: Sun, 28 Apr 2024 18:31:09 GMT
• Title: Pragmatic Formal Verification of Sequential Error Detection and Correction Codes (ECCs) used in Safety-Critical Design
• Authors: Aman Kumar,
• Abstract summary: ECCs are often used in digital designs to protect data integrity. Exhaustive verification of ECC using formal methods has been a challenge. We present a pragmatic formal verification approach of complex ECC cores.
• Score: 3.1367764768902613
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Error Detection and Correction Codes (ECCs) are often used in digital designs to protect data integrity. Especially in safety-critical systems such as automotive electronics, ECCs are widely used and the verification of such complex logic becomes more critical considering the ISO 26262 safety standards. Exhaustive verification of ECC using formal methods has been a challenge given the high number of data bits to protect. As an example, for an ECC of 128 data bits with a possibility to detect up to four-bit errors, the combination of bit errors is given by 128C1 + 128C2 + 128C3 + 128C4 = 1.1 * 10^7. This vast analysis space often leads to bounded proof results. Moreover, the complexity and state-space increase further if the ECC has sequential encoding and decoding stages. To overcome such problems and sign-off the design with confidence within reasonable proof time, we present a pragmatic formal verification approach of complex ECC cores with several complexity reduction techniques and know-how that were learnt during the course of verification. We discuss using the linearity of the syndrome generator as a helper assertion, using the abstract model as glue logic to compare the RTL with the sequential version of the circuit, k-induction-based model checking and using mathematical relations captured as properties to simplify the verification in order to get an unbounded proof result within 24 hours of proof runtime.

Related papers

• Accelerating Error Correction Code Transformers [56.75773430667148]
  We introduce a novel acceleration method for transformer-based decoders. We achieve a 90% compression ratio and reduce arithmetic operation energy consumption by at least 224 times on modern hardware.
  arXiv  Detail & Related papers  (2024-10-08T11:07:55Z)
• 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)
• Fast Context-Biasing for CTC and Transducer ASR models with CTC-based Word Spotter [57.64003871384959]
  This work presents a new approach to fast context-biasing with CTC-based Word Spotter. The proposed method matches CTC log-probabilities against a compact context graph to detect potential context-biasing candidates. The results demonstrate a significant acceleration of the context-biasing recognition with a simultaneous improvement in F-score and WER.
  arXiv  Detail & Related papers  (2024-06-11T09:37:52Z)
• 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)
• Testing the Accuracy of Surface Code Decoders [55.616364225463066]
  Large-scale, fault-tolerant quantum computations will be enabled by quantum error-correcting codes (QECC) This work presents the first systematic technique to test the accuracy and effectiveness of different QECC decoding schemes.
  arXiv  Detail & Related papers  (2023-11-21T10:22:08Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  We propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core.
  arXiv  Detail & Related papers  (2023-08-15T13:19:17Z)
• Fault-Tolerant Computing with Single Qudit Encoding [49.89725935672549]
  We discuss stabilizer quantum-error correction codes implemented in a single multi-level qudit. These codes can be customized to the specific physical errors on the qudit, effectively suppressing them. We demonstrate a Fault-Tolerant implementation on molecular spin qudits, showcasing nearly exponential error suppression with only linear qudit size growth.
  arXiv  Detail & Related papers  (2023-07-20T10:51:23Z)
• Adaptive Planning Search Algorithm for Analog Circuit Verification [53.97809573610992]
  We propose a machine learning (ML) approach, which uses less simulations. We show that the proposed approach is able to provide OCCs closer to the specifications for all circuits.
  arXiv  Detail & Related papers  (2023-06-23T12:57:46Z)
• Concurrent Classifier Error Detection (CCED) in Large Scale Machine Learning Systems [10.839595991409828]
  We introduce Concurrent Error Detection (CCED), a scheme to implement CED in Machine Learning systems. CCED identifies a set of check signals in the main ML system and feeds them to the concurrent ML that is trained to detect errors. Results show that more than 95 percent of the errors are detected when using a simple Random Forest classifier.
  arXiv  Detail & Related papers  (2023-06-02T12:36:05Z)
• PAC-Based Formal Verification for Out-of-Distribution Data Detection [4.406331747636832]
  This study places probably approximately correct (PAC) based guarantees on OOD detection using the encoding process within VAEs. It is used to bound the detection error on unfamiliar instances with user-defined confidence.
  arXiv  Detail & Related papers  (2023-04-04T07:33:02Z)
• Deep Quantum Error Correction [73.54643419792453]
  Quantum error correction codes (QECC) are a key component for realizing the potential of quantum computing. In this work, we efficiently train novel emphend-to-end deep quantum error decoders. The proposed method demonstrates the power of neural decoders for QECC by achieving state-of-the-art accuracy.
  arXiv  Detail & Related papers  (2023-01-27T08:16:26Z)

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.