2025-09-01から1ヶ月間の記事一覧
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 …
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 ビットスーパースカラマイクロプロセッサである。動的アウトオ…
