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
LiteXではじめる自作SoC(1)
LiteX ではじめる自作SoC 最近は、RISC-V の誕生により、CPUコアは個人の趣味で作るのが難しくない時代になってきた。 さて、コンピュータというのは、CPUコアだけで動くものではなく、周辺のストレージ、ネットワーク、DRAM、USB、その他入出力装置が揃ってはじめて動くものだ。 CPUコアが個人で自由に作れるようになったら、その次のステップとして、周辺装置も含めた物体、つまり、SoC(System On Chip)を自分で作れるようになりたいと思うのは自然なことだろう。 LiteX は、そういうSoCを自分で作ってみたいという人向けのツール、RTLなどが集まったプロジェクトだ。 公式のWikiによると、 LiteX is a Python "front-end" that generates Verilog netlists, and drives proprietary bu
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
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
YoWASP
GitHub - BrunoLevy/learn-fpga: Learning FPGA, yosys, nextpnr, and RISC-V
GitHub - kazkojima/colorlight-i5-tips: Tiny tips for Colorlight i5 FPGA board
GitHub - YosysHQ/apicula: Project Apicula 🐝: bitstream documentation for Gowin FPGAs
Analyze PicoRV32 - HackMD
GitHub - tillitis/tillitis-key1: FPGA verilog and firmware for TKey, the flexible and open USB security key 🔑
CXXRTL, a Yosys Simulation Backend
Getting Started with ECP5 FPGAs on the Colorlight i5 FPGA Development Board
A fun Friday evening--verifying an AXI-lite slave
The ZipCPU by Gisselquist Technology
https://www.mouser.jp/new/quicklogic/quicklogic-eos-s3-mcu-efpga-socs/