論文の概要: An Executable Formal Model of the VHDL in Isabelle/HOL
- arxiv url: http://arxiv.org/abs/2202.04192v1
- Date: Tue, 8 Feb 2022 23:10:25 GMT
- ステータス: 処理完了
- システム内更新日: 2022-02-11 03:06:05.259449
- Title: An Executable Formal Model of the VHDL in Isabelle/HOL
- Title(参考訳): Isabelle/HOLにおけるVHDLの実行可能な形式モデル
- Authors: Wilayat Khan, Zhe Hou, David Sanan, Jamel Nebhen, Yang Liu, Alwen Tiu
- Abstract要約: We define a formal model of the VHDL language in Isabelle/HOL。
我々のモデルは、産業で使われているVHDL設計の機能的部分、特にLEON3プロセッサの整数ユニットの設計をターゲットとしている。
我々のモデルはOCamlコードにエクスポートして実行し、形式モデルをVHDLシミュレータに変換する。
- 参考スコア(独自算出の注目度): 4.025825303202995
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In the hardware design process, hardware components are usually described in
a hardware description language. Most of the hardware description languages,
such as Verilog and VHDL, do not have mathematical foundation and hence are not
fit for formal reasoning about the design. To enable formal reasoning in one of
the most commonly used description language VHDL, we define a formal model of
the VHDL language in Isabelle/HOL. Our model targets the functional part of
VHDL designs used in industry, specifically the design of the LEON3 processor's
integer unit. We cover a wide range of features in the VHDL language that are
usually not modelled in the literature and define a novel operational semantics
for it. Furthermore, our model can be exported to OCaml code for execution,
turning the formal model into a VHDL simulator. We have tested our simulator
against simple designs used in the literature, as well as the div32 module in
the LEON3 design. The Isabelle/HOL code is publicly available:
https://zhehou.github.io/apps/VHDLModel.zip
- Abstract(参考訳): ハードウェア設計プロセスでは、ハードウェアコンポーネントは通常、ハードウェア記述言語で記述される。
verilogやvhdlといったハードウェア記述言語の多くは数学的基礎を持っておらず、そのため設計に関する形式的な推論には適していない。
最も一般的な記述言語であるVHDLにおける形式的推論を可能にするため、Isabelle/HOLでVHDL言語の形式的モデルを定義する。
我々のモデルは、産業で使用されるvhdl設計の機能、特にleon3プロセッサの整数ユニットの設計をターゲットとしている。
VHDL言語では、典型的には文献でモデル化されていない幅広い特徴をカバーし、それのための新しい操作意味論を定義する。
さらに、我々のモデルはOCamlコードにエクスポートして実行し、形式モデルをVHDLシミュレータに変換する。
文献で使われている単純な設計とLEON3設計のdiv32モジュールに対してシミュレータを試験した。
isabelle/holコード: https://zhehou.github.io/apps/vhdlmodel.zip
関連論文リスト
- StarCoder 2 and The Stack v2: The Next Generation [105.93298676368798]
私たちは3.3から4.3兆のトークンで3B、7B、15BパラメータでStarCoder2モデルをトレーニングします。
我々は、それらをCode LLMベンチマークの包括的なセットで徹底的に評価する。
私たちの大きなモデルであるStarCoder2-15Bは、同等の大きさの他のモデルよりも大幅に優れています。
論文 参考訳(メタデータ) (2024-02-29T13:53:35Z) - If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code
Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される
コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
論文 参考訳(メタデータ) (2024-01-01T16:51:20Z) - LLM4EDA: Emerging Progress in Large Language Models for Electronic
Design Automation [74.7163199054881]
大規模言語モデル(LLM)は、文脈理解、論理推論、回答生成においてその能力を実証している。
本稿では,EDA分野におけるLLMの応用に関する系統的研究を行う。
論理合成,物理設計,マルチモーダル特徴抽出,回路のアライメントにLLMを適用することに焦点を当て,今後の研究の方向性を強調した。
論文 参考訳(メタデータ) (2023-12-28T15:09:14Z) - CLadder: Assessing Causal Reasoning in Language Models [82.8719238178569]
我々は,大言語モデル (LLM) が因果関係をコヒーレントに説明できるかどうかを検討する。
ユデア・パールらによって仮定された「因果推論エンジン」にインスパイアされた、自然言語における因果推論という新たなNLPタスクを提案する。
論文 参考訳(メタデータ) (2023-12-07T15:12:12Z) - LLMSTEP: LLM proofstep suggestions in Lean [27.5626664686618]
LLMSTEPはLean 4の戦術で、ユーザの証明状態を言語モデルをホストするサーバに送る。
言語モデルは提案を生成し、リーンでチェックされ、開発環境でユーザに表示される。
論文 参考訳(メタデータ) (2023-10-27T20:10:56Z) - What's Left? Concept Grounding with Logic-Enhanced Foundation Models [76.74146485832125]
本稿では,ドメインに依存しない一階述語論理型プログラムを用いて,ドメイン間の概念を基礎と推論するために学習する統一フレームワークを提案する。
LEFTは,2次元画像,3次元シーン,人間の動き,ロボット操作という4つの領域で,柔軟に概念を学習する。
論文 参考訳(メタデータ) (2023-10-24T17:50:20Z) - Scope is all you need: Transforming LLMs for HPC Code [5.0227775038998415]
本稿では,HPCにおける前処理やコンパイル中心のタスクに特化して設計された,Tokompilerという新しいトークン機構を提案する。
Tokompilerは言語プリミティブの知識を活用して、言語指向のトークンを生成し、コード構造をコンテキスト対応で理解する。
その結果、Tokompilerは従来のトークン化ツールに比べてコード補完精度と意味理解を著しく向上させることがわかった。
論文 参考訳(メタデータ) (2023-08-18T10:12:03Z) - Chip-Chat: Challenges and Opportunities in Conversational Hardware
Design [27.760832802199637]
人工知能(AI)は、マシンベースのエンドツーエンド翻訳の能力を実証した。
LLM(Large Language Models)は、様々なプログラミング言語でコードを生成することができると主張している。
この「チップチャット」は、私たちが世界で初めて完全にAIで書かれたテープアウト用HDLだと信じているものになったと信じています。
論文 参考訳(メタデータ) (2023-05-22T17:13:33Z) - Towards A Visual Programming Tool to Create Deep Learning Models [15.838427479984926]
DeepBlocksは、Deep Learning開発者が特定のプログラミング言語に頼ることなく、モデルを設計、トレーニング、評価できるビジュアルプログラミングツールである。
我々は5人の参加者による形式的なインタビューから設計目標を導出し、典型的なユースケースを通じてツールの最初の実装を検証した。
論文 参考訳(メタデータ) (2023-03-22T16:47:48Z) - Formal Specifications from Natural Language [3.1806743741013657]
本稿では,自然言語を複雑な意味を持つ形式仕様に翻訳する言語モデルについて検討する。
特に、構造化英語文からなる3つのデータセット上で、オフザシェルフ言語モデルを微調整する。
論文 参考訳(メタデータ) (2022-06-04T10:49:30Z) - A Systematic Evaluation of Large Language Models of Code [88.34057460577957]
コードの大規模な言語モデル(LM)は、最近、コードを完成させ、自然言語記述からコードを合成する大きな可能性を示しています。
現在の最先端のコードLMは公開されておらず、モデルやデータ設計の決定について多くの疑問が残されている。
Codexはオープンソースではありませんが、既存のオープンソースモデルはいくつかのプログラミング言語でクローズな結果が得られることが分かりました。
GPT-2アーキテクチャに基づいた2.7Bパラメータを持つ新しいモデルPolyCoderをリリースし、12のプログラミング言語を1台のマシンで249GBのコードでトレーニングした。
論文 参考訳(メタデータ) (2022-02-26T15:53:55Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。