論文の概要: Pragmatic Formal Verification of Sequential Error Detection and Correction Codes (ECCs) used in Safety-Critical Design

• arxiv url: http://arxiv.org/abs/2404.18270v1
• Date: Sun, 28 Apr 2024 18:31:09 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-30 15:16:10.633525
• Title: Pragmatic Formal Verification of Sequential Error Detection and Correction Codes (ECCs) used in Safety-Critical Design
• Title（参考訳）: 安全臨界設計における逐次誤り検出・訂正符号(ECC)の実用的形式検証
• Authors: Aman Kumar,
• Abstract要約: ECCは、データ完全性を保護するためにしばしばデジタル設計で使用される。 形式的手法によるECCの排他的検証が課題となっている。 複素ECCコアの実用的形式検証手法を提案する。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 誤り検出訂正符号(ECC)は、データ整合性を保護するためにしばしばデジタル設計で使用される。 特に自動車エレクトロニクスなどの安全クリティカルなシステムでは、ECCが広く使われ、ISO 26262の安全基準を考えると、そのような複雑な論理の検証がより重要になる。 形式的手法によるECCの排他的検証は、保護すべきデータビットの多さを考えると困難である。 例えば、128ビットのデータビットのECCで最大4ビットエラーを検出する場合、ビットエラーの組み合わせは128C1 + 128C2 + 128C3 + 128C4 = 1.1 * 10^7で与えられる。 この広大な解析空間は、しばしば有界な証明結果をもたらす。 さらに、ECCがシーケンシャルエンコーディングおよびデコードステージを持つ場合、複雑さと状態空間はさらに増加する。 このような問題を克服し、妥当な証明時間内に設計を信頼してサインオフするために、複雑なECCコアの実用的形式的検証手法と、検証期間中に学習したノウハウを提案する。 そこで,本論文では,シンドローム生成器の線形性をヘルパーアサーションとして使用し,抽象モデルを用いてRTLを回路の逐次バージョンと比較し,k-インダクションに基づくモデルチェックを行い,数学的関係を特性として捉え,検証を単純化し,24時間以内の証明結果を得る。

関連論文リスト

• Fast Context-Biasing for CTC and Transducer ASR models with CTC-based Word Spotter [57.64003871384959]
  この研究は、CTCベースのWord Spotterでコンテキストバイアスを高速化するための新しいアプローチを示す。 提案手法は,CTCログ確率をコンパクトなコンテキストグラフと比較し,潜在的なコンテキストバイアス候補を検出する。 その結果、FスコアとWERの同時改善により、文脈バイアス認識の大幅な高速化が示された。
  論文  参考訳（メタデータ） (2024-06-11T09:37:52Z)
• Pragmatic Formal Verification Methodology for Clock Domain Crossing (CDC) [2.3624953088402734]
  本稿では,Clock Domain Crossings (CDC) 問題を最小化するための実用的形式検証手法の開発に焦点をあてる。 CDCは、転移性効果の傾向があり、そのようなCDCの機能的検証は、バグの回避を確実にするために非常に重要である。
  論文  参考訳（メタデータ） (2024-04-20T13:17:25Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。 このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。 我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
  論文  参考訳（メタデータ） (2024-01-02T03:37:11Z)
• Testing the Accuracy of Surface Code Decoders [55.616364225463066]
  大規模でフォールトトレラントな量子計算は量子エラー訂正符号(QECC)によって実現される 本研究は,QECC復号方式の精度と有効性をテストするための最初の体系的手法である。
  論文  参考訳（メタデータ） (2023-11-21T10:22:08Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。 この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。 あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
  論文  参考訳（メタデータ） (2023-08-15T13:19:17Z)
• Fault-Tolerant Computing with Single Qudit Encoding [49.89725935672549]
  単一マルチレベルキューディットに実装された安定化器量子エラー訂正符号について論じる。 これらのコードは、quditの特定の物理的エラーに合わせてカスタマイズすることができ、効果的にそれらを抑制することができる。 分子スピン四重項上のフォールトトレラントな実装を実証し、線形キューディットサイズのみの成長を伴うほぼ指数関数的な誤差抑制を示す。
  論文  参考訳（メタデータ） (2023-07-20T10:51:23Z)
• Adaptive Planning Search Algorithm for Analog Circuit Verification [53.97809573610992]
  シミュレーションの少ない機械学習(ML)アプローチを提案する。 提案手法により,OCCを全回路の仕様に近づけることができることを示す。
  論文  参考訳（メタデータ） (2023-06-23T12:57:46Z)
• Concurrent Classifier Error Detection (CCED) in Large Scale Machine Learning Systems [10.839595991409828]
  本稿では,CEDを機械学習システムに実装するCED(Concurrent Error Detection)を提案する。 CCEDはメインMLシステムの一連のチェック信号を識別し、エラーを検出するために訓練された同時MLにフィードする。 その結果、単純なランダムフォレスト分類器を使用すると、95%以上のエラーが検出されることがわかった。
  論文  参考訳（メタデータ） (2023-06-02T12:36:05Z)
• PAC-Based Formal Verification for Out-of-Distribution Data Detection [4.406331747636832]
  本研究は、VAEの符号化プロセスを用いて、OOD検出に基づくほぼ正しい(PAC)保証を行う。 ユーザ定義の信頼性で不慣れなインスタンスに検出エラーをバインドするために使用される。
  論文  参考訳（メタデータ） (2023-04-04T07:33:02Z)
• Deep Quantum Error Correction [73.54643419792453]
  量子誤り訂正符号(QECC)は、量子コンピューティングのポテンシャルを実現するための鍵となる要素である。 本研究では,新しいエンペンド・ツー・エンドの量子誤りデコーダを効率的に訓練する。 提案手法は,最先端の精度を実現することにより,QECCのニューラルデコーダのパワーを実証する。
  論文  参考訳（メタデータ） (2023-01-27T08:16:26Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。