2025-09-01から1ヶ月間の記事一覧
前回はこちら： msyksphinz.hatenablog.com 前回の失敗を反映しながら、最終的に以下の形になった： `ifdef FORMAL always_comb begin if ($initstate) begin assume(r_sim_priority_oh == 'h1); assume(w_sim_priority_oh_next == 'h1); assume(r_pri_accep…
SymbiYosysの能力を検証するために、簡単なサンプルデザインを作ってフォーマル検証を行っていく。 前回実装したアービタを検証するために、フォーマルの記述を追加していく： logic [N-1: 0] r_sim_priority_oh; logic [N-1: 0] w_sim_priority_oh_next; lo…
SymbiYosysの能力を検証するために、簡単なサンプルデザインを作ってフォーマル検証を行っていく。 まずは、以下のような形のラウンドロビンアービタを作ったうえで、機能検証を行う。 module rr_arbiter2 #( parameter N = 4 ) ( input logic i_clk, input …
github.com module cc_onehot #( parameter int unsigned Width = 4 ) ( input logic [Width-1:0] d_i, output logic is_onehot_o ); ... localparam int LVLS = $clog2(Width) + 1; logic [LVLS-1:0][2**(LVLS-1)-1:0] sum, carry; logic [LVLS-2:0] carry_…
SystemVerilogで実装されたECCエンコーダー(ecc_encode.sv)の実装詳細について解析する。 この実装は、SECDED(Single Error Correction, Double Error Detection)ハミング符号を使用しており、1ビットのエラーを自動的に訂正し、2ビットのエラーを検出する能…
riscv-formalフレームワークを使用してCLZ命令の動作を検証する。 riscv-formalでの検証設定 1. 検証用テストケースの作成 insns/insn_clz.vを作成して、CLZ命令の検証用テストケースを定義した： module rvfi_insn_clz ( input clock, input reset, `RVFI_I…
前回の記事では、riscv-formalフレームワークを使用してVexRiscvの動作確認を行った。今回は、RISC-V Zbb拡張のCLZ（Count Leading Zeros）命令をVexRiscvに実装し、riscv-formalで検証する。 CLZ命令は、RISC-V Zbb拡張（Bit Manipulation Extension）に含…
PULPのCommon Cellsを読んでみようプロジェクト、まずは動作の理解が簡単そうな グリッチフリーのクロック切り替え回路について見てみよう。 github.com 概要 (モジュールのヘッダより) clk_mux_glitch_freeは、完全に未知の位相関係を持つN個の任意の入力ク…
Pulpのcommon cellsにどういうものが入っているのかを、ChatGPTに纏めてもらった。この記事は、概要を知りたいだけのもの。 github.com 概要テーブル カテゴリ モジュール名 ファイル名 概要 リンク アドレスデコーダ addr_decode addr_decode.sv アドレスマ…
ハードウェア設計において、複数のリクエストが同時に発生した際に、どのリクエストを優先するかを決定するアービタは非常に重要なコンポーネントだ。 ETH Zurichのcommon_cellsライブラリに含まれるrr_arb_tree.svの実装について詳しく見ていくことにした。…
https://yosyshq.readthedocs.io/projects/riscv-formal/en/latest/procedure.html の部分について、わかることをまとめていく。 yosyshq.readthedocs.io Verification procedure RISC-V Formalのテストは、ISA準拠性を検証するために実行されるものである。…
VexRiscv におけるriscv-formal の実行方法を調査している。 前回の続き： msyksphinz.hatenablog.com insn_addi_ch0 にのみ注力して 動作を確認する 以下のコマンドで、insn_addi_ch0に注力して動作を確認する。 make -C checks insn_addi_ch0 make -C chec…
VexRiscv におけるriscv-formal の実行方法を調査している。 前回の続き：msyksphinz.hatenablog.com 例えば、 rvfi_insn_addi は以下のようにインスタンス化されている。それぞれのフォーマルの項目に対してインスタンスが作られているようだ。 insns/isa_r…
VexRiscv におけるriscv-formal の実行方法を調査している。 github.com riscv-formal proofs for VexRiscv Current state: Test a simple VexRiscv configuration: https://github.com/SpinalHDL/VexRiscv/blob/master/src/main/scala/vexriscv/demo/Formal…
NERV: シングルステージのR32I のプロセッサ。 PicoRV32: RV32IMCを実装したRISC-Vコア。パイプライン化されているかどうかは謎。 SERV: ビットシリアル実装のRV32Iプロセッサ。きわめてシンプル。 VexRiscv: SpinalHDLで生成されたRV32Iプロセッサ。 このラ…
前回の続きだ。メモリアクセスの検証用インタフェースについて見てみよう。 msyksphinz.hatenablog.com 外部メモリバスの処理 RISC-V Formalの仕様では、RVFI経由で観測されるコアが生じさせるメモリアクセスと、それに伴って発生するデータバス上で観測され…
RISC-V Formal Verification Frameworkは、RISC-Vプロセッサの形式的検証を行うための包括的なフレームワークである。 このフレームワークは、RISC-V Formal Interface (RVFI)を中心として構築されており、SystemVerilog Assertions (SVA)を活用した形式的テ…
RISC-V Formal Verification Frameworkは、RISC-Vプロセッサの形式的検証を行うための包括的なフレームワークである。 このフレームワークは、RISC-V Formal Interface (RVFI)を中心として構築されており、SystemVerilog Assertions (SVA)を活用した形式的テ…
"The MIPS R10000 Superscalar Microprocessor" の論文をもう一度読み直してみている。 1. 概要 MIPS R10000 は、シリコン・グラフィックス社 (Silicon Graphics, Inc.) によって開発された 64 ビットスーパースカラマイクロプロセッサである。動的アウトオ…
