論文の概要: Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL

• arxiv url: http://arxiv.org/abs/2607.23715v1
• Date: Sun, 26 Jul 2026 15:26:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-28 22:34:15.208885
• Title: Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL
• Title（参考訳）: ARCH HDLにおける形式的検証可能な浮動小数点データ型
• Abstract要約: 本稿では,ARCHのための一級IEEE-754 binary32 (FP32) と bfloat16 (BF16) 演算の設計とエンドツーエンド検証について報告する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: We report the design and end-to-end verification of first-class IEEE-754 binary32 (FP32) and bfloat16 (BF16) arithmetic for ARCH, a hardware description language intended to be generated by language models. Every operator - comparisons, conversions, add, sub, mul, and fused multiply-add (FMA) - is described once against a single bit-vector IR and rendered three ways from one source: synthesizable SystemVerilog, an SMT-LIB model, and a Lean 4 proof model. The three artifacts cannot drift apart structurally, and the residual per-node printer correspondence is machine-checked: a Yosys-to-SMT miter proves the emitted SystemVerilog equivalent to the SMT model for all 24 operators. Verification splits at the solver-tractability frontier: multiplier-free operators (comparisons, add/sub over all 2^64 inputs, conversions, and all binary BF16 arithmetic) are proved exhaustively equivalent to the SMT-LIB FloatingPoint theory; the SAT-hard multiplier-bearing operators (FP32 mul and FMA) are proved correctly rounded in Lean, sorry-free, against a value-level round-to-nearest-even specification over exact dyadic values. Physical characterization exposed the FMA as the timing outlier: its exact-wide 470-bit datapath does not pipeline in our flow. We reimplemented it as a bounded 98-bit guard/round/sticky datapath that pipelines to 268 MHz on Nangate45, and proved, in Lean and over all 2^96 inputs, that it is bit-identical to the exact-wide reference, so it inherits the reference's proven correct rounding. The equivalence is tractable precisely because the shared multiplier appears on both sides and cancels: neither a SAT solver nor the proof ever solves a multiplier equivalence. (The BF16 FMA is deliberately an FP32-accumulating fusion, characterized as exactly that.) All machine-checked claims are pinned to a tagged open-source release.
• Abstract（参考訳）: 本稿では,言語モデルによるハードウェア記述言語ARCHのための一級IEEE-754 binary32(FP32)とbfloat16(BF16)演算の設計とエンドツーエンド検証について報告する。 すべての演算子(比較、変換、加算、サブ、mul、融合乗算加算(FMA))は、1つのビットベクターIRに対して一度記述され、1つのソースから3つの方法で描画される:synthesizable SystemVerilog、SMT-LIBモデル、Lean 4証明モデル。 3つのアーティファクトは構造的に分解できず、残りのノードごとのプリンタ対応はマシンチェックされる: Yosys-to-SMTミッターは、24の演算子すべてに対してSMTモデルと同等の出力されたSystemVerilogを証明する。 乗算子なし作用素 (2^64入力、変換、および全てのバイナリBF16演算子) は、SMT-LIB FloatingPoint理論と排他的に等価であることが証明され、SAT-hard乗算作用素 (FP32 mul と FMA) は、正確なdyadic値に対する値レベルのラウンド・トゥ・アレスト・セブン仕様に対してリーンで正しく丸められている。 470ビットの正確なデータパスは、私たちのフローをパイプラインしない。 98ビットガード/ラウンド/スティッキーなデータパスとして再実装し、Nangate45で268MHzにパイプラインし、Leanおよび2^96のすべての入力において、正確な参照に対してビット識別可能であることを証明した。 共有乗算器が両側に現れてキャンセルされるため、同値性は正確に抽出可能であり、SATソルバも証明も乗算器同値性は解けない。 (BF16 FMAは意図的にFP32の累積核融合であり、まさにそのように特徴付けられる) マシンチェックされたクレームはすべて、タグ付けされたオープンソースリリースにピン留めされる。

関連論文リスト

• FoldNTT: A Multiplier- and Twiddle-Lean NTT Core with Formally Verified Arithmetic for Proth Primes [0.0]
  FoldNTTはRadix-2NTTアクセラレータ(TCHES 2022)の再設計である 完全にオープンな流れでArtix-7では、バタフライあたり3>1 DSP48、フルコアのFmaxで保存されたツイドルビットが約4%である。
  論文  参考訳（メタデータ） (2026-09-06T06:09:50Z)
• Transformer Accelerator (TFA): A Macro-Op INT8 Hardware Chip for Transformer Inference and Machine Translation [0.3882135185458233]
  Transformer Accelerator (TFA) は、Transformer推論のためのシンセサイザー可能な、パラメータ化可能なINT8メモリ・ツー・メモリエンジンである。 TFAは行列乗法、ソフトマックス、RMSNorm、要素演算、コピー/ガザ演算を8つの512ビットマクロ-op記述子で実装している。 RTLは出力定常多重累積配列と、DMAと計算の重なり合うピンポンバッファ、ビットエクサクサク逆二乗根と分割単位、キー値キャッシュと埋め込みアドレス処理、およびアボトセーフゼロパディング書き込みエンジンを結合する。
  論文  参考訳（メタデータ） (2026-08-06T06:59:25Z)
• Constrained Decoding for Diffusion Language Models via Efficient Inference over Finite Automata [57.27430779838529]
  有限オートマトンとして表現可能な任意の制約の下で,制約付き平均場後部からサンプリングする,正確かつトラクタブルなアルゴリズムを提案する。 このアプローチは、構築による制約満足度を保証し、欲求とサンプリングベースのデコーディングの両方をサポートし、並列およびブロックワイドデコーディングと互換性がある。 Dream-7B と LLaDA-8 の実証的な評価は、様々なタスクにおいてかなりの精度の向上を示した。
  論文  参考訳（メタデータ） (2026-07-08T05:48:57Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。 VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
  論文  参考訳（メタデータ） (2026-05-08T14:20:06Z)
• BWTA: Accurate and Efficient Binarized Transformer by Algorithm-Hardware Co-design [71.97035034203275]
  バイナライゼーションにおけるゼロ点歪みを解析し,BWTA量子化方式を提案する。 本稿では,Smooth Multi-Stage Quantizationを提案し,レベルワイド・デグラデーション・ストラテジーとMagnitude Alignment Projection Factorを組み合わせた。 実験の結果、BWTAはTransformerベースのモデルに対して、GLUEでは平均3.5%、タスクでは2%未満の精度でフル精度のパフォーマンスにアプローチしていることがわかった。
  論文  参考訳（メタデータ） (2026-04-05T04:25:07Z)
• NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference [0.0]
  LLM推論を検証可能なゼロ知識証明システムであるメソッドを提案する。 我々のアプローチは、トランスフォーマー推論が自然に独立した層計算に分解されるという事実を生かしている。 EZKLと比較して、EZKLは70倍小さい証明と5.7倍速い証明時間をd=128で達成し、形式的な音質保証を維持している。
  論文  参考訳（メタデータ） (2026-03-17T04:14:45Z)
• Residual Context Diffusion Language Models [90.07635240595926]
  Residual Context Diffusion (RCD) は、捨てられたトークン表現をコンテキスト残留に変換し、次のデノイングステップでそれらを注入するモジュールである。 RCDは、最小限の計算オーバーヘッドで、5-10ポイントの精度でフロンティアdLLMを一貫して改善する。
  論文  参考訳（メタデータ） (2026-01-30T13:16:32Z)
• LLM.int8(): 8-bit Matrix Multiplication for Transformers at Scale [80.86029795281922]
  トランスにおけるフィードフォワードおよびアテンションプロジェクション層に対するInt8行列乗算法を開発した。 175Bパラメータ16/32ビットのチェックポイントをロードし、Int8に変換し、直ちに使用することができる。
  論文  参考訳（メタデータ） (2022-08-15T17:08:50Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) と Transformer は、自然言語処理タスクに使用される2つの一般的なニューラルネットワークアーキテクチャである。 実際には、トランスフォーマーモデルの方がLSTMよりも表現力が高いことがよく見られる。 本研究では,LSTMとTransformerの実践的差異について検討し,その潜在空間分解パターンに基づく説明を提案する。
  論文  参考訳（メタデータ） (2021-12-16T19:56:44Z)
• I-BERT: Integer-only BERT Quantization [78.43819756382103]
  トランスフォーマーモデルのための新しい量子化手法であるI-BERTを提案する。 I-BERTは浮動小数点演算なしでエンドツーエンドの整数のみのBERT推論を実行する。 いずれの場合も,I-BERTは全精度ベースラインと同等(かつ若干高い)精度が得られた。
  論文  参考訳（メタデータ） (2021-01-05T02:42:58Z)

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

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