RISC-V Formal Verification Framework (riscv-formal) についてまとめる - FPGA開発日記
RISC-V Formal Verification Frameworkは、RISC-Vプロセッサの形式的検証を行うための包括的なフレームワークである。 このフレームワークは、RISC-V Formal Interface (RVFI)を中心として構築されており、SystemVerilog Assertions (SVA)を活用した形式的テストベンチを提供する。 riscv-formalの目的と意義 riscv-formalの主な目的は、RISC-Vプロセッサの機能的正確性を数学的に証明することである。 従来のシミュレーションベースの検証では、テストケースの網羅性に依存するため、バグの見落としが発生する可能性がある。 一方、形式的検証では、全ての可能な入力と状態遷移を数学的に検証することで、プロセッサの正確性を保証できる。 RISC-V Formal Interface (RVFI) の概
SymbiYosysのドキュメントを読む (6. 検証が失敗するケースの練習問題) - FPGA開発日記
SymbiYosysによるデザイン検証の続き：FIFOの検証で、検証が失敗するケースをデバッグする。 symbiyosys.readthedocs.io 練習問題 [script] nofullskip: read -define NO_FULL_SKIP=1 noverific: read -noverific read -formal fifo.sv hierarchy -check -top fifo -chparam MAX_DATA 17 prep -top fifo 追加したhierarchyコマンドは、トップ・モジュールのMAX_DATAパラメーターを17に変更する。basicタスクを実行し、何が起こるか見てみよう。Assert failed in fifo: a_count_diff のようなエラーが出るはず。すべてのテストに合格しながら、MAX_DATAのより大きな値で動
SymbiYosysのドキュメントを読む (5. FIFOの検証のカバーケースを観察する) - FPGA開発日記
SymbiYosysによるデザイン検証の続き：FIFOの検証例で、カバーケースを取得する方法を見てみる。 正しい動作の間、w_underfillステートメントはアンダーフローのケースをカバーする。fifo_cover/logfile.txtを調べると、探しているcoverステートメントを含むトレースファイルがわかる。このファイルが存在しない場合は、以下のコードを実行する。 $ sby fifo.sby cover w_underfill というのはこれかな (追記：違った。実際には https://msyksphinz.hatenablog.com/entry/2025/05/18/040000 に書いたとおり、もっとシンプルなプロパティが動作していた) // use block formatting for w_underfill so it's easier to describe i
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (1. SymbiYosysのインストールと基本的な動作確認) - FPGA開発日記
オープンソース・ツールを用いた形式検証を行いたくて、いろいろチュートリアルを読んでいる。 例えば、以下の記事で書いてあるようなBRAMの形式検証を行ってみたい。 zipcpu.com デザインとしては以下をそのまま利用してみる： github.com デザインの本体： always @(posedge w_clk) begin if(w_en) bram[w_addr] <= w_data; end always @(posedge r_clk) begin if(r_en) r_data <= bram[r_addr]; end Formalのassertionの部分 assume()によって、探索の範囲を小さくする： symbiyosys.readthedocs.io // set data variable to whats in the bram initial begin ass
GitHub - Wren6991/Hazard3: 3-stage RV32IMACZb* processor with debug
Hazard3 is a 3-stage RISC-V processor, implementing the RV32I instruction set and the following optional extensions: M: integer multiply/divide/modulo A : atomic memory operations, with AHB5 global exclusives C: compressed instructions Zicsr: CSR access Zba: address generation Zbb: basic bit manipulation Zbc: carry-less multiplication Zbs: single-bit manipulation Zbkb: basic bit manipulation for s
技術資料 | アートグラフィックス
SystemVerilog言語に関する知識はもはや常識となりました。弊社の技術資料は、SystemVerilogを業務で的確に使用する為の補助資料として、あらゆるレベルの技術者に役立つ様に準備されています。UVMも IEEE 規格となり、UVMに関する知識は、既に、常識化しつつあります。弊社の技術資料は、SystemVerilogとUVMに関する最新知識を得る目的に最適です。 SystemVerilogによる検証の基礎（検証技術者向け） SystemVerilog言語仕様書は容易に理解できる英文で書かれていないだけでなく、多くの表現には深い意味が込められており、単なる通読では見落としてしまう機能が多々存在します。特に、検証に関わる機能においての不正確な理解は致命的な問題に発展してしまいます。本書は、初心者が陥り易い問題を未然に防ぐ為に、特筆すべき機能に関しては詳細な技術解説と使用例を添えて
GitHub - google/xls: XLS: Accelerated HW Synthesis
XLS implements a High Level Synthesis toolchain that produces synthesizable designs (Verilog and SystemVerilog) from flexible, high-level descriptions of functionality. It is Apache 2 licensed. XLS (Accelerated HW Synthesis) aims to be the Software Development Kit (SDK) for the End of Moore's Law (EoML) era. In this "age of specialization", software and hardware engineers must do more co-design ac
半導体設計について何も知らない素人が1ヶ月で8bitCPUをテープアウトした話 - 抹茶うまい
この記事は HDL Advent Calendar 2021 25日目の記事です。 すいません、11日ほど遅れての投稿です。 この記事では、以下のツイートに至るまでの裏話について話させていただきます。 HDLに関係があるかというとかなーり微妙ですが、許していただきたいです🙏 Our first tapeout project of 8bit CPU with @Cra2yPierr0t has just finished. We still don't have enough knowledge about making LSI ...https://t.co/J99bRlMTY3#mpw3 #efabless #openmpw pic.twitter.com/6MmGvlDMCZ— Δyuk! (@heppoko_yuki) 2021年11月12日 遂に@heppoko_yuki と共
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - WangXuan95/FPGA-USB-Device: An FPGA-based USB 1.1 (full-speed) device core to implement USB-serial, USB-camera, USB-audio, USB-hid, etc. It requires only 3 FPGA common IOs rather than additional chips. 基于FPGA的USB 1.1 (full-speed) device端控制器，可实现US
fpga-verilog.md
GitHub - WangXuan95/FPGA-HDMI: An FPGA-based HDMI display controller. 基于FPGA的HDMI显示控制器
GitHub - Learning-Chips-Lab/OpenEye: The Open Source Hardware Accelerator for Efficient Neural Network Inference
GitHub - chipsalliance/synlig: SystemVerilog synthesis tool
GitHub - zachjs/sv2v: SystemVerilog to Verilog conversion
GitHub - YosysHQ/sby: SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
My Personal Journey in Verification
GitHub - olofk/serv: SERV - The SErial RISC-V CPU
GitHub - ulixxe/usb_cdc: Single/Multi-channel Full Speed USB interface for FPGA and ASIC designs
GitHub - ultraembedded/core_usb_cdc: Basic USB-CDC device core (Verilog)
CXXRTL, a Yosys Simulation Backend