論文の概要: Analogous Alignments: Digital "Formally" meets Analog
- arxiv url: http://arxiv.org/abs/2409.15013v1
- Date: Mon, 23 Sep 2024 13:38:31 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-26 14:53:59.796312
- Title: Analogous Alignments: Digital "Formally" meets Analog
- Title（参考訳）: アナログアライメント:デジタル"形式"がアナログに一致する
- Authors: Hansa Mohanty, Deepak Narayan Gadde,
- Abstract要約: 本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。
Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 現代のSystem-on-Chips(SoCs)の複雑さは継続的に増加しており、短期間で信頼性の高いチップを市場に投入することはますます困難になっている。
特に、設計の実現可能性を研究することを目的としたテストチップの場合、時間は重要な要素である。
プレシリコン機能検証は、製品開発サイクルの大部分を構成する主要なコントリビュータの1つです。
検証エンジニアはしばしば、シリコン上で非機能であることが判明したテストチップを緩やかに検証する。
検証の取り組みを左シフトするために、形式的検証は設計を徹底的に検証し、全体的な品質をより信頼することを目的とした強力な方法論である。
本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。
本稿では,アナログ行動モデルを形式的検証設定に組み込む新しいアプローチについて論じる。
Digital and Analog Mixed-Signal (AMS) は、本質的に異なる設計であり、形式的な検証設定においてシームレスに統合される。
我々のフォーマルなセットアップは、FPV、CSR検証、接続性チェックといった強力なフォーマルなテクニックを活用しています。
FPVに使用されるプロパティは、メタモデリングフレームワークを使用して自動生成される。
また, 状態空間の爆発, AMS モデルとの形式的適合性, k-induction などの緩和技術といった課題についても論じる。
この検証アプローチでは、適切な時間と十分なカバレッジで、設計を徹底的に検証することが可能でした。
また、早い段階でいくつかのバグを報告し、完全な設計検証プロセスを反復的かつ効果的にしました。
関連論文リスト
- Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。
まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。
第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
論文 参考訳（メタデータ） (2024-10-24T06:09:40Z) - Pragmatic Formal Verification Methodology for Clock Domain Crossing (CDC) [2.3624953088402734]
本稿では,Clock Domain Crossings (CDC) 問題を最小化するための実用的形式検証手法の開発に焦点をあてる。
CDCは、転移性効果の傾向があり、そのようなCDCの機能的検証は、バグの回避を確実にするために非常に重要である。
論文 参考訳（メタデータ） (2024-04-20T13:17:25Z) - A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs [2.655207969975261]
System-on-Chips (SoC) の大半は開発サイクルを短縮するために知的財産(IP)を利用している。
膨大な数の可能性が、残酷な力によるアプローチを許さない。
本稿では,効率的な構成カバレッジを実現するための半形式的検証手法を提案する。
論文 参考訳（メタデータ） (2024-04-20T12:18:47Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。
我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T21:53:32Z) - HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。
ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。
本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。
論文 参考訳（メタデータ） (2023-09-14T19:24:57Z) - Representing Timed Automata and Timing Anomalies of Cyber-Physical
Production Systems in Knowledge Graphs [51.98400002538092]
本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。
モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
論文 参考訳（メタデータ） (2023-08-25T15:25:57Z) - Improving Text Matching in E-Commerce Search with A Rationalizable,
Intervenable and Fast Entity-Based Relevance Model [78.80174696043021]
エンティティベース関連モデル(EBRM)と呼ばれる新しいモデルを提案する。
この分解により、高精度にクロスエンコーダQE関連モジュールを使用できる。
また、ユーザログから自動生成されたQEデータによるQEモジュールの事前トレーニングにより、全体的なパフォーマンスが向上することを示す。
論文 参考訳（メタデータ） (2023-07-01T15:44:53Z) - Precision-Recall Divergence Optimization for Generative Modeling with
GANs and Normalizing Flows [54.050498411883495]
本研究では,ジェネレーティブ・アドバイサル・ネットワークや正規化フローなどの生成モデルのための新しいトレーニング手法を開発した。
指定された精度-リコールトレードオフを達成することは、textitPR-divergencesと呼ぶ家族からのユニークな$f$-divergenceを最小化することを意味する。
当社のアプローチは,ImageNetなどのデータセットでテストした場合の精度とリコールの両面で,BigGANのような既存の最先端モデルの性能を向上させる。
論文 参考訳（メタデータ） (2023-05-30T10:07:17Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems [20.491263196235376]
我々は,ロボット工学の分野で広く利用されている学習可能な状態推定システム(LE-SESs)に注目した。
LE-SESを形式的検証の観点から検討し,システムモデルの満足度を決定する。
論文 参考訳（メタデータ） (2020-10-16T11:06:50Z) - Automated and Formal Synthesis of Neural Barrier Certificates for
Dynamical Models [70.70479436076238]
バリア証明書(BC)の自動的,形式的,反例に基づく合成手法を提案する。
このアプローチは、ニューラルネットワークとして構造化されたBCの候補を操作する誘導的フレームワークと、その候補の有効性を認証するか、反例を生成する音検証器によって支えられている。
その結果,音のBCsを最大2桁の速度で合成できることがわかった。
論文 参考訳（メタデータ） (2020-07-07T07:39:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。