論文の概要: 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
関連論文リスト
- The Llama 3 Herd of Models [356.6353861669039]
本稿ではLlama 3と呼ばれる新しい基礎モデルについて述べる。
Llama 3は、多言語性、コーディング、推論、ツール使用をサポートする言語モデルの群れである。
Llama 3は、GPT-4のような主要な言語モデルに匹敵する品質を多くのタスクで提供しています。
論文 参考訳（メタデータ） (2024-07-31T17:54:27Z) - VHDL-Eval: A Framework for Evaluating Large Language Models in VHDL Code Generation [4.700008016247411]
本稿では,VHDLコード生成タスクの評価に特化して設計された包括的評価フレームワークを提案する。
このデータセットは、Verilog評価問題の集合をVHDLに翻訳し、公開されているVHDL問題を集約することにより、合計202の問題を発生させる。
生成したVHDL符号の機能的正当性を評価するために, 自己検証テストベンチのキュレートセットを利用する。
論文 参考訳（メタデータ） (2024-06-06T00:06:50Z) - Xmodel-VLM: A Simple Baseline for Multimodal Vision Language Model [7.082567506213992]
本稿では,最先端のマルチモーダル視覚言語モデルであるXmodel-VLMを紹介する。
コンシューマGPUサーバへの効率的なデプロイのために設計されている。
論文 参考訳（メタデータ） (2024-05-15T09:47:59Z) - Evaluating LLMs for Hardware Design and Test [25.412044293834715]
大規模言語モデル(LLM)は、ハードウェア記述言語(HDL)でコードを生成する能力を実証した。
機能的および検証目的でVerilogを生成する際に,最先端の会話型LLMの機能と限界について検討する。
論文 参考訳（メタデータ） (2024-04-23T18:55:49Z) - HDLdebugger: Streamlining HDL debugging with Large Language Models [20.09481664579469]
チップ設計の分野では、ハードウェア記述言語(HDL)が重要な役割を果たしている。
大規模言語モデル(LLM)のソフトウェアコードの生成、完成、検査における強力な能力にもかかわらず、HDLデバッグの専門分野における利用は制限されている。
本稿では, 逆エンジニアリング手法によるHDLデータ生成, 検索拡張生成のための検索エンジン, 検索拡張LDMファインチューニング手法によるHDLgerというフレームワークを提案する。
HDLgerはHuaweiから提供されたHDLコードデータセットで実施した実験により,HDLgerが13件の切断に優れていることが判明した。
論文 参考訳（メタデータ） (2024-03-18T11:19:37Z) - 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) - Chip-Chat: Challenges and Opportunities in Conversational Hardware
Design [27.760832802199637]
人工知能(AI)は、マシンベースのエンドツーエンド翻訳の能力を実証した。
LLM(Large Language Models)は、様々なプログラミング言語でコードを生成することができると主張している。
この「チップチャット」は、私たちが世界で初めて完全にAIで書かれたテープアウト用HDLだと信じているものになったと信じています。
論文 参考訳（メタデータ） (2023-05-22T17:13:33Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。