Masayuki @ FPGA開発日記
LightNews LightNews
masayukik.bsky.social
Masayuki @ FPGA開発日記
@masayukik.bsky.social
21 followers 13 following 450 posts
https://msyksphinz.hatenablog.com/
Posts Replies Media Videos
masayukik.bsky.social
Design Solution Forum 2025の発表資料をアップロードしました。

speakerdeck.com/msyksphinz/o...
オープンソースでどこまでできる？フォーマル検証チャレンジ
近年、EDAツールの分野でもオープンソース化が進み、フォーマル検証にも無償で利用できる環境が登場しています。 本講演ではSymbiYosysを使った論理回路レベルのフォーマル検証に挑戦し、その有効性や限界を実例と共に紹介します。 さらにCPU設計への応用としてriscv-formalとRVFIを…
speakerdeck.com
October 8, 2025 at 2:35 PM
masayukik.bsky.social
Design Solution Forum 2025で登壇します。

「オープンソースでどこまでできる？フォーマル検証チャレンジ」 10/07(火) 16:20–16:50 @ Room D

- フォーマル検証の基礎
- Round-Robin Arbiterなど簡単なデザインの検証
- RISC-Vコアへの応用事例
October 4, 2025 at 1:50 AM
masayukik.bsky.social
www.eetimes.com/mips-ceo-acq...
mips.com/press-releas...
mips.com/blog/mips-an...
www.eetimes.com
July 8, 2025 at 2:06 PM
masayukik.bsky.social
Codasipといい、ここ数日動きが激しい。

gf.com/gf-press-rel...
GlobalFoundries to Acquire MIPS to Accelerate AI and Compute Capabilities  | GlobalFoundries to Acquire MIPS
Acquisition will expand GF portfolio with cutting-edge RISC-V processor IP and software tools for real-time computing in autonomous mobility, industrial automation, datacenter and intelligent edge app...
gf.com
July 8, 2025 at 1:42 PM
masayukik.bsky.social
今年の初めからずっと予約受付中になってて、直近だとリリース予定が7月になってと思って今見てみたら8/12にさらに伸びててひっくり返った。いつ出版されるんだ。

shop.elsevier.com/books/comput...
Computer Architecture
Computer Architecture: A Quantitative Approach, has been considered essential reading by instructors, students and practitioners of computer design fo
shop.elsevier.com
June 30, 2025 at 4:18 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
riscv-isadocの命令一覧表を改修する (2. 浮動小数点の章をアップデート) - FPGA開発日記
msyksphinz-self.github.io riscv-isadoc ドキュメントの浮動小数点命令に関する章をアップデートした。 今回の改訂では、命令フォーマットの図示に WaveDrom を導入し、ビットフィールドの構造や動作の流れをより直感的に理解できるようにした。
msyksphinz.hatenablog.com
June 29, 2025 at 3:52 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
Integrating Prefetcher Selection with Dynamic Request Allocation Improves Prefetching Efficiencyを読む (1) - FPGA開発日記
HPCA 2025で発表された以下の論文を読んでみることにした。 www.computer.org Integrating Prefetcher Selection with Dynamic Request Allocation Improves Prefetching Efficiency 日本語訳: 動的リクエスト割当を統合したプリフェッチャ・セレクションを統合することによるプリフェッチ効率の...
msyksphinz.hatenablog.com
June 28, 2025 at 4:07 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
ジャンプの依存関係を可視化する objdump --visualize-jumps=extended-color の活用法 - FPGA開発日記
GNU Binutils に含まれる objdump には、アセンブリのジャンプ命令の依存関係を視覚的に表示する --visualize-jumps という非常に興味深い機能が存在する。 --visualize-jumps とは objdump コマンドはバイナリファイルを逆アセンブルして人間が読める形で表示するツールであるが、--visualize-jumps オプションを付与することで、ジャン...
msyksphinz.hatenablog.com
June 27, 2025 at 4:07 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
RISC-VのZkt拡張について調べる - FPGA開発日記
「Zkt拡張」は、暗号処理やセキュリティ分野で重要な役割を果たす拡張である。Zkt拡張について調べてみよう。 github.com Zkt拡張は、RISC-Vプロセッサにおいて「定数時間（constant-time）」で動作することが保証される命令のサブセットを定義する拡張である。 ここでいう定数時間とは、命令の実行時間が入力データに依存しないことを意味する。 これにより、タイミングサイドチャネル...
msyksphinz.hatenablog.com
June 26, 2025 at 3:15 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
RISC-V の ZfhおよびZfhmin拡張について調べる - FPGA開発日記
RVA23で追加されている、Zfh拡張及びZfhmin拡張について調べている。ドキュメントを読みながら、まとめていこう。 これらはIEEE 754-2008規格に準拠した16ビット半精度浮動小数点命令を提供する拡張である。 Zfh拡張の概要 Zfh拡張は、16ビット半精度浮動小数点(half-precision)命令を追加するものであり、単精度浮動小数点拡張(F拡張)に依存している。 NaN Bo...
msyksphinz.hatenablog.com
June 25, 2025 at 3:21 PM
masayukik.bsky.social
Renewal: msyksphinz-self.github.io/riscv-isadoc/

msyksphinz.hatenablog.com/entry/2025/0...
riscv-isadocの命令一覧表を改修する - FPGA開発日記
今のriscv-isadocのHTMLページはsphinxで作ってあるから、以下のようなイメージだ。 msyksphinz-self.github.io これを以下のように改修している。 やりたいこととしてはAsciidocを使って書き直すのと、WaveDromを使って命令の表記を変えることなので、これでうまくいくはずだ。 追記：https://msyksphinz-self.github.io/...
msyksphinz.hatenablog.com
June 22, 2025 at 1:18 AM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...

msyksphinz.hatenablog.com/entry/2025/0...
AXIのWRAPバースト転送について理解を深める (1. 公式ドキュメントの確認) - FPGA開発日記
AXIのWRAPバースト転送について、あまり理解が深くなかったため、改めて勉強してみることにした。 まずは公式ドキュメントの内容を確認していこう。 developer.arm.com WRAPバースト転送とは WRAPバースト転送は、インクリメントバーストと似た性質を持つが、上限アドレスに達した際に下位アドレスに折り返すという特徴がある。この転送方式には、以下のような制約が存在する。 開始アドレス...
msyksphinz.hatenablog.com
June 17, 2025 at 4:51 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (12. BMCモードにおけるFIFOの検証) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 形式検証ツールSymbiYosysを用いたFIFOの検証 検証対象のFIFO 検証対象としたFIFOは、以下の特徴を持つシンプルな実装である： データ幅：8ビット（パラメータ化可能） エントリ数：4 制御信号：プッシュ（書き込み）、ポップ（読み出し） 状態信号：...
msyksphinz.hatenablog.com
June 15, 2025 at 4:51 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (11. BMCモードにおけるエンジンとオプション) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysのBMCモードにおけるエンジンとオプション SymbiYosys（sby）のBMCモードでは、様々なエンジンとオプションを使用することができる。 BMCモードの基本設定 BMCモードを使用する場合は、以下のように設定する。 [options]...
msyksphinz.hatenablog.com
June 13, 2025 at 4:47 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (10. ラウンドロビンアービタを検証する) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 ラウンドロビンアービタに、検証項目を追加してみる。 より詳細なアサーションを追加して検証してみよう。以下は、expected_grant()を追加して、今の優先度情報とリクエストの情報によりどの信号が有効化されるはずかを示した関数を追加している。 この情報を使っ...
msyksphinz.hatenablog.com
June 13, 2025 at 4:47 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (9. ラウンドロビンアービタを検証する) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysでラウンドロビンアービタを検証する: 検証エンジンの変更 検証が完了しないため、別のSMTソルバーを使用してみることにした。以下のように設定を変更した： [engines] # smtbmc yices smtbmc boolector # ...
msyksphinz.hatenablog.com
June 13, 2025 at 4:46 PM
masayukik.bsky.social
もらった。わーい
June 12, 2025 at 12:14 AM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (9. ラウンドロビンアービタを検証する) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysでラウンドロビンアービタを検証する: 検証エンジンの変更 検証が完了しないため、別のSMTソルバーを使用してみることにした。以下のように設定を変更した： [engines] # smtbmc yices smtbmc boolector # ...
msyksphinz.hatenablog.com
June 11, 2025 at 4:22 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (8. ラウンドロビンアービタを検証する) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysでラウンドロビンアービタを検証する ラウンドロビンアービタは、複数のリクエストを公平に処理するための回路である。 SystemVerilogで実装したラウンドロビンアービタを、形式検証ツールであるSymbiYosysを使用して検証してみる。 ...
msyksphinz.hatenablog.com
June 11, 2025 at 4:03 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
SnipersimのPentium M分岐予測器の実装を読む (1. 分岐予測器の構成) - FPGA開発日記
github.com Pentium M プロセッサの分岐予測器アーキテクチャを模した実装を解析していく。この分岐予測器は、複数の予測器を組み合わせたハイブリッド型の設計となっている。 1. クラスの構成要素 class PentiumMBranchPredictor : public BranchPredictor { public: PentiumMBranchPredictor(String...
msyksphinz.hatenablog.com
June 10, 2025 at 4:01 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (7. BMCからUMCへの変更) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysを使った乗算器の形式検証 乗算器の検証の続き。 msyksphinz.hatenablog.com BMCからUMCへの変更 Bounded Model Checking (BMC)から、Unbounded Model Checking (U...
msyksphinz.hatenablog.com
June 10, 2025 at 2:15 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (6. 乗算器の検証2) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysを使った乗算器の形式検証 乗算器の検証の続き。 msyksphinz.hatenablog.com デザインの修正 デザインを修正した。修正後のコードは以下の通りである。 module mult ( input logic [ 7: 0] a...
msyksphinz.hatenablog.com
June 10, 2025 at 10:20 AM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (5. 乗算器の検証) - FPGA開発日記
カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000 SymbiYosysを使った乗算器の形式検証 SymbiYosysを使用して乗算器の形式検証を行ってみる。 検証対象の乗算器 検証対象の乗算器は以下のようなVerilogコードで記述されている。8ビットの入力a, bを受け取り、16ビットの出力mを生成する単純な...
msyksphinz.hatenablog.com
June 10, 2025 at 10:18 AM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
RISC-V LinuxをBusyBox付きでビルドするDocker環境の構築 (1. Dockerfileの作成) - FPGA開発日記
RISC-V Linuxのビルド環境を構築するにあたり、以下の目標を設定した。 RISC-V LinuxカーネルとBusyBoxを自前でビルドし、QEMU上で動作させる ホスト環境を汚さず、Dockerコンテナ内で完結させる なるべく自動化して、再現性の高い環境を構築する 2. Dockerfileの構築 まずはベースとなるDockerfileを用意する。 Ubuntu 24.04をベースに、RI...
msyksphinz.hatenablog.com
June 8, 2025 at 4:51 PM
masayukik.bsky.social
msyksphinz.hatenablog.com/entry/2025/0...
RISC-VのSBI（Supervisor Binary Interface）の仕組みと役割についての調査 - FPGA開発日記
最近RISC-VのLinuxサポート周りを調べている中で、「SBI(Supervisor Binary Interface)」という仕組みが要所で登場する。 最初は「ブート時の一時的なインターフェースかな？」と思っていたが、どうやらRISC-Vにおいてはランタイムでも重要な役割を持つ仕組みであることが分かってきた。 ここでは、SBIの基本的な仕組みと役割に加え、x86との対比を通してこの設計の意図...
msyksphinz.hatenablog.com
June 8, 2025 at 2:01 PM