カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysを使った乗算器の形式検証 SymbiYosysを使用して乗算器の形式検証を行ってみる。 検証対象の乗算器 検証対象の乗算器は以下のようなVerilogコードで記述されて…

RISC-V Linuxのビルド環境を構築するにあたり、以下の目標を設定した。 RISC-V LinuxカーネルとBusyBoxを自前でビルドし、QEMU上で動作させる ホスト環境を汚さず、Dockerコンテナ内で完結させる なるべく自動化して、再現性の高い環境を構築する 2. Dockerf…

最近RISC-VのLinuxサポート周りを調べている中で、「SBI(Supervisor Binary Interface)」という仕組みが要所で登場する。 最初は「ブート時の一時的なインターフェースかな？」と思っていたが、どうやらRISC-Vにおいてはランタイムでも重要な役割を持つ仕組…

github.com この辺の実装がどのようになっているのかを勉強したい。ChatGPTにお願いしながら、読み進めていくことにする。 msyksphinz.hatenablog.com 4. 閾値(theta)の動的調整 adjust_threshold(prediction_correct); adjust_thresholdは次のように定義さ…

github.com この辺の実装がどのようになっているのかを勉強したい。ChatGPTにお願いしながら、読み進めていくことにする。 msyksphinz.hatenablog.com テーブルのアップデート方法 void hashed_perceptron::last_branch_result(champsim::address pc, champs…

github.com この辺の実装がどのようになっているのかを勉強したい。ChatGPTにお願いしながら、読み進めていくことにする。 msyksphinz.hatenablog.com 5. テーブルと内積計算(std::inner_product) result.yout = std::inner_product( std::begin(tables), st…

github.com この辺の実装がどのようになっているのかを勉強したい。ChatGPTにお願いしながら、読み進めていくことにする。 msyksphinz.hatenablog.com 予測の実行 bool hashed_perceptron::predict_branch(champsim::address pc) { auto get_index = [pc_sli…

github.com この辺の実装がどのようになっているのかを勉強したい。ChatGPTにお願いしながら、読み進めていくことにする。 msyksphinz.hatenablog.com ghist_words：折り畳みシフトレジスタ（folded_shift_register） using history_type = folded_shift_reg…

github.com この辺の実装がどのようになっているのかを勉強したい。ChatGPTにお願いしながら、読み進めていくことにする。 Hashed Perceptronのテーブルの定義 using bits = champsim::data::bits; // saves some typing constexpr static std::size_t NTABL…

msyksphinz.hatenablog.com sgとwsgのファイルフォーマットについてだいぶ把握したので、Graph-Vのベンチマークにこれを組み込んで動かせるようにしてみよう。 repo.hca.bsc.es ポイントは、VecGraphの構築時にファイル名に応じてsg/wsgの読み込みコードを挿…

msyksphinz.hatenablog.com sgファイルについて調査したので、次はwsgファイルだ。wsg(weighted serialized graph) ファイルは、重み付きなので、各エッジに重みの情報が付くことになる。 wsgファイルの構造 wsgファイルを読み取るときのプログラムは以下の…

sgファイルについてもうちょっと見てみることにした： sgファイルの構造 sgファイルを読み取るときのプログラムは以下のようになっている： vector_benches/gapbs/src/reader.h bool directed; SGOffset num_nodes, num_edges; DestID_ **index = nullptr, *…

GAP(Graph Algorithm Platform)ベンチマークは、グラフアルゴリズムの性能評価に広く用いられている。 その際、グラフデータの格納や配布のために独自の圧縮ファイル形式である.sgや.wsgが利用されている。 これらのファイル形式の概要と特徴について調査す…

SymbiYosysによるデザイン検証の続き。 symbiyosys.readthedocs.io 前回のブログの記事には一部誤解があり、SymbiYosysは以下のコードを実行できない。実際には、実行するにはTabby CAD Suiteのライセンスが必要なようだ。 // use block formatting for w_un…

SymbiYosysによるデザイン検証の続き：FIFOの検証で、検証が失敗するケースをデバッグする。 symbiyosys.readthedocs.io 練習問題 [script] nofullskip: read -define NO_FULL_SKIP=1 noverific: read -noverific read -formal fifo.sv hierarchy -check -to…

SymbiYosysによるデザイン検証の続き：FIFOの検証例で、カバーケースを取得する方法を見てみる。 正しい動作の間、w_underfillステートメントはアンダーフローのケースをカバーする。fifo_cover/logfile.txtを調べると、探しているcoverステートメントを含む…

これはいろいろ試行錯誤中にはまってしまったのだが、たとえば40GB近くのファイルをRISC-Vのプログラムで処理したい場合、Spikeを使うときにいろいろと詰まった。 普通にriscv64-unknown-elf-gccを使ってコンパイルすると、これはnewlibを使っているからか知…

msyksphinz.hatenablog.com msyksphinz.hatenablog.com GCC15.1にすると、Newlibのビルドが失敗する問題なのだが、バージョンを落としてGCC14.3ならば正しくビルドできることが分かった。 これがなぜなのか理由が良く分からない。正直GCCのリビジョンの違い…

msyksphinz.hatenablog.com 以前GCC13.1を使ってOfficial GCCを使ったRISC-V向けGCCの構築方法をメモしていたのだが、これをGCC15.1に更新するとトラブルが発生した。 問題はNewlibのビルド部分だ： curl -L ftp://sourceware.org/pub/newlib/newlib-4.5.0.2…

https://github.com/msyksphinz-self/symbiyosys-docker-env に、SymbiYosysを含めた試行環境を置いておくことにした。 github.com 以下は、SymbiYosys（SBY）およびその依存ツール（Yosys、yosys-smtbmc、Boolectorなど）をインストールした検証用Dockerfil…

SymbiYosysのドキュメントを読むために、まずはリポジトリ内のドキュメントを読んでみることにする。 github.com SymbiYosysでFIFOサンプルを検証しようとした際の実行ログを以下に示す。 なんか思っているのと違うなあ。VCDファイルも生成されていない。 sb…

msyksphinz.hatenablog.com BlueSky認証情報の管理 前回の実装には問題が残っていた。 BSKY_DID と BSKY_JWT は定期的に更新される必要があるため、スクリプトを改良する必要があった。 BlueSkyの認証情報について、ChatGPTに詳しく説明してもらった： BSKY_…

X(Twitter)は最近もう使っていないので、はてなブログの投稿をBlueSkyに投稿させたい。 このためにはBlueSkyのAPIを叩いたり、はてなブログから記事情報を引っ張ってきて投稿文章を作成しないといけない。 しかし自分はそのあたりのWebアプリケーション周り…

msyksphinz.hatenablog.com 各チャネルについて、AXI5/AXI4でどのようなバリエーションがあるかまとめていきたい。Rチャネル。 (この図は仕様書を読みながら自分で作ったので、誤解により間違いがあるかもしれない) Signal AXI5 AXI5-Lite AXI4 AXI4-Lite AX…

msyksphinz.hatenablog.com 各チャネルについて、AXI5/AXI4でどのようなバリエーションがあるかまとめていきたい。ARチャネル。 (この図は仕様書を読みながら自分で作ったので、誤解により間違いがあるかもしれない) Signal AXI5 AXI5-Lite AXI4 AXI4-Lite A…

SymbiYosysのドキュメントを読むために、まずはリポジトリ内のドキュメントを読んでみることにする。 github.com まずはFIFOに関するドキュメントを読んでみよう。DeepLの力を借りて翻訳しながら読んでいく。 symbiyosys.readthedocs.io FIFO (First-In, Fir…

msyksphinz.hatenablog.com 各チャネルについて、AXI5/AXI4でどのようなバリエーションがあるかまとめていきたい。Bチャネル。 (この図は仕様書を読みながら自分で作ったので、誤解により間違いがあるかもしれない) Signal AXI5 AXI5-Lite AXI4 AXI4-Lite AX…

msyksphinz.hatenablog.com 各チャネルについて、AXI5/AXI4でどのようなバリエーションがあるかまとめていきたい。Wチャネルから。 (この図は仕様書を読みながら自分で作ったので、誤解により間違いがあるかもしれない) Signal AXI5 AXI5-Lite AXI4 AXI4-Lit…

msyksphinz.hatenablog.com 各チャネルについて、AXI5/AXI4でどのようなバリエーションがあるかまとめていきたい。まずはAWチャネルから。 (この図は仕様書を読みながら自分で作ったので、誤解により間違いがあるかもしれない) Signal AXI5 AXI5-Lite AXI4 A…

AXI5/AXI4のそれぞれのバリエーションについてまとめてみる。 AWチャネルの信号リスト Wチャネルの信号リスト Bチャネルの信号リスト ARチャネルの信号リスト Rチャネルの信号リスト AXI5 もっとも汎用的なパラメータを持つもの。 AXI5-Lite AXI5のサブセッ…