論文の概要: 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 などの緩和技術といった課題についても論じる。 この検証アプローチでは、適切な時間と十分なカバレッジで、設計を徹底的に検証することが可能でした。 また、早い段階でいくつかのバグを報告し、完全な設計検証プロセスを反復的かつ効果的にしました。

関連論文リスト

• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。 既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。 そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-12-26T07:53:41Z)
• Quantum-Adversary-Resilient Evidence Structures and Migration Strategies for Regulated AI Audit Trails [0.0]
  一定サイズの暗号証拠記録は、臨床、薬品、財務設定において、規制されたAIワークロードのための監査証跡を構築するために、ますます使用されている。 しかし、既存のインスタンス化は、量子能力のある敵によって長期のセキュリティが脅かされる古典的なシグネチャスキームに依存している。 本稿では,量子敵の存在下でのエビデンス構造に対するセキュリティ概念を定式化し,デプロイされた監査ログに対するポスト量子インスタンス化とマイグレーション戦略について検討する。
  論文  参考訳（メタデータ） (2025-11-27T12:57:44Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  線形木探索はLarge Language Model (LLM) 研究の基盤となっている。 本稿では,検索アルゴリズムを3つのコアコンポーネントに分解する統合フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-11T03:29:18Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Lightweight Task-Oriented Semantic Communication Empowered by Large-Scale AI Models [66.57755931421285]
  大規模人工知能(LAI)モデルは、リアルタイム通信シナリオにおいて重大な課題を提起する。 本稿では,LAIモデルから知識を抽出・凝縮するために知識蒸留(KD)技術を活用することを提案する。 本稿では,反復推論の必要性を排除したプレストア圧縮機構を備えた高速蒸留法を提案する。
  論文  参考訳（メタデータ） (2025-06-16T08:42:16Z)
• 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)

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

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