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
Yosys Fronts For Xilinx ISE
We always marvel at how open-source tools can often outstrip their commercial counterparts. Yosys, the open-source tool for Verilog synthesis, is a good example. Although the Xilinx ISE design suite is something close to abandonware, a lot of people still use it because it supports older FPGAs the newer tools don’t. Its Verilog parser is somewhat slow to catch up to new standards, and according to
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
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
CXXRTL, a Yosys Simulation Backend
The ZipCPU by Gisselquist Technology
https://www.youtube.com/channel/UC1kyKOb_sv52OfVTZW5WXPg
iCE40 FPGA Toolchain on Linux
icestorm/examples/icestick/rs232demo.v at master · YosysHQ/icestorm
GitHub - grahamedgecombe/icicle: 32-bit RISC-V system on chip for iCE40 FPGAs
GitHub - AleksandarKostovic/Riscy-SoC: Riscy-SoC is SoC based on RISC-V CPU core, designed in Verilog
Under the hood of Formal Verification
Symbiotic EDA – tools to make digital designers more productive
YosysHQ SBY documentation