論文の概要: Verifying Non-friendly Formal Verification Designs: Can We Start Earlier?

• arxiv url: http://arxiv.org/abs/2410.18454v1
• Date: Thu, 24 Oct 2024 06:09:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-25 16:43:36.826724
• Title: Verifying Non-friendly Formal Verification Designs: Can We Start Earlier?
• Title（参考訳）: 非フレンドリな形式検証設計の検証:早く始められるか?
• Authors: Bryan Olmos, Daniel Gerl, Aman Kumar, Djones Lettnin,
• Abstract要約: 本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。 まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。 第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
• 参考スコア（独自算出の注目度）: 2.1626093085892144
• License:
• Abstract: The design of Systems on Chips (SoCs) is becoming more and more complex due to technological advancements. Missed bugs can cause drastic failures in safety-critical environments leading to the endangerment of lives. To overcome these drastic failures, formal property verification (FPV) has been applied in the industry. However, there exist multiple hardware designs where the results of FPV are not conclusive even for long runtimes of model-checking tools. For this reason, the use of High-level Equivalence Checking (HLEC) tools has been proposed in the last few years. However, the procedure for how to use it inside an industrial toolchain has not been defined. For this reason, we proposed 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; the advantage of this step is that the assertions at the software level run in seconds and we can start our analysis with conclusive results about our algorithm before starting to write the RTL (Register Transfer Level) design. Second, this algorithmic description is verified against its sequential design using HLEC and the respective metamodel parameters. The results show that the presented methodology can find bugs early related to the algorithmic description and prepare the setup for the HLEC verification. This helps to reduce the verification efforts to set up the tool and write the properties manually which is always error-prone. The proposed framework can help teams working on datapaths to verify and make decisions in an early stage of the verification flow.
• Abstract（参考訳）: チップのシステム(SoC)の設計は、技術進歩によりますます複雑になりつつある。 欠落したバグは、生命の危険に繋がる安全クリティカルな環境で劇的な失敗を引き起こす可能性がある。 このような劇的な失敗を克服するために、業界ではフォーマルなプロパティ検証(FPV)が適用されている。 しかし、モデルチェックツールの長期実行時でさえ、FPVの結果は決定的ではない複数のハードウェア設計が存在する。 このため、ここ数年でHLEC(High-level Equivalence Checking)ツールが提案されている。 しかし、産業ツールチェーン内でそれを使用する手順は定義されていない。 そこで我々は,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。 まず、C++で書かれた未使用のアルゴリズム記述を、生成したアサーションを使用して早期に検証する。このステップの利点は、ソフトウェアレベルでのアサーションが数秒で実行され、RTL(Register Transfer Level)設計を始める前に、アルゴリズムに関する決定的な結果から分析を開始することができることである。 第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。 その結果,提案手法はアルゴリズム記述に関連するバグを早期に発見し,HLEC検証の準備が可能であることがわかった。 これにより、ツールをセットアップし、常にエラーが発生しているプロパティを手動で記述する検証作業の削減に役立ちます。 提案されたフレームワークは、検証フローの初期段階において、データパスに取り組むチームが検証と決定を行うのに役立つ。

関連論文リスト

• Enabling Unit Proofing for Software Implementation Verification [2.7325338323814328]
  本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
  論文  参考訳（メタデータ） (2024-10-18T18:37:36Z)
• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。 Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
  論文  参考訳（メタデータ） (2024-09-23T13:38:31Z)
• A Lean Transformer Model for Dynamic Malware Analysis and Detection [0.0]
  マルウェアは現代のコンピューティングの世界にとって急速に成長する脅威であり、既存の防衛線はこの問題に対処するのに十分な効率性を持っていない。 これまでの研究では、実行レポートから抽出したニューラルネットワークとAPI呼び出しシーケンスを活用することに成功した。 本稿では,悪意のあるファイルを検出するために,Transformersアーキテクチャに基づくエミュレーションオンリーモデルを設計する。
  論文  参考訳（メタデータ） (2024-08-05T08:46:46Z)
• Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification [0.09786690381850355]
  制約付きホーンクロース(CHC)は、従来、形式的検証において低レベルな表現として用いられてきた。 線形CHCに対する別のボトムアップ手法を提案し、オープンソースのモデルチェックフレームワーク THETA における2つの選択肢を評価する。
  論文  参考訳（メタデータ） (2024-04-23T16:46:27Z)
• Automated Static Warning Identification via Path-based Semantic Representation [37.70518599085676]
  本稿では、深層ニューラルネットワークの強力な特徴抽出と表現能力を用いて、警告識別のための制御フローグラフパスからコードセマンティクスを生成する。 事前訓練された言語モデルを微調整し、パスシーケンスを符号化し、モデル構築のための意味表現をキャプチャする。
  論文  参考訳（メタデータ） (2023-06-27T15:46:45Z)
• Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
  本研究では,不確実性に関する情報を伝達することで,プログラマがより迅速かつ正確にコードを生成することができるかどうかを検討する。 トークンのハイライトは、編集される可能性が最も高いので、タスクの完了が早くなり、よりターゲットを絞った編集が可能になることがわかりました。
  論文  参考訳（メタデータ） (2023-02-14T18:43:34Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。 AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
  論文  参考訳（メタデータ） (2021-09-25T22:53:24Z)
• FCOS: A simple and strong anchor-free object detector [111.87691210818194]
  物体検出を画素ごとの予測方式で解くために, 完全畳み込み型一段物検出器 (FCOS) を提案する。 RetinaNet、SSD、YOLOv3、Faster R-CNNといった最先端のオブジェクト検出器のほとんどは、事前に定義されたアンカーボックスに依存している。 対照的に、提案した検出器FCOSはアンカーボックスフリーであり、提案はフリーである。
  論文  参考訳（メタデータ） (2020-06-14T01:03:39Z)
• End-to-End Object Detection with Transformers [88.06357745922716]
  本稿では,オブジェクト検出を直接セット予測問題とみなす新しい手法を提案する。 我々のアプローチは検出パイプラインを合理化し、手作業で設計された多くのコンポーネントの必要性を効果的に除去する。 この新しいフレームワークの主な構成要素は、Detection TRansformerまたはDETRと呼ばれ、セットベースのグローバルな損失である。
  論文  参考訳（メタデータ） (2020-05-26T17:06:38Z)
• Pre-training Is (Almost) All You Need: An Application to Commonsense Reasoning [61.32992639292889]
  事前学習されたトランスモデルの微調整は、一般的なNLPタスクを解決するための標準的なアプローチとなっている。 そこで本研究では,可視性ランキングタスクをフルテキスト形式でキャストする新たなスコアリング手法を提案する。 提案手法は, ランダム再起動にまたがって, より安定した学習段階を提供することを示す。
  論文  参考訳（メタデータ） (2020-04-29T10:54:40Z)

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

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