Simple system: three assertion failures in a four-state simulation (config small)

オープン
  • 何か問題がありますか？
#2,577 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 2 日以内に返信

まだ誰も着手していません。

評価

難易度
4/5
見積もり時間
3〜5日
初心者へのやさしさ
42/100
issue の種類
バグ
明瞭さ
おおむね明確
活発さ
活発
領域
embedded-iot, testing

調査の方向性

Start with the named assertions in ibex_core.sv, prim_fifo_sync.sv, and ibex_top.sv, then trace the simple system configuration in ibex_simple_system.sv and the RAM response behavior in prim_ram_2p. Reproduce with the small configuration and a four-state simulator using hello_test or CoreMark, with VERILATOR undefined so assertions run. Done when the root causes are addressed and these simulations no longer report the failures while program output remains correct.

索引モデルが issue の本文から書いたものです。

説明

Ibex at commit 626034d7 (also checked against master db2b0d9c, which changes only Nix files), with the CHERIoT support (ibex_cheriot_pkg, gen_cheriot_trvk),
examples/simple_system, configuration small (util/ibex_config.py small), compiled without VERILATOR so that the
SVA assertions are active, running examples/sw/simple_system/hello_test and examples/sw/benchmarks/coremark.
The program output is correct (CoreMark: "Correct operation validated"). Two four-state simulators report the same failures at the same times:

Assertion hello_test CoreMark Cause
IllegalParamCHERIoTNoWriteback (ibex_core.sv:2475) 1 1 configuration (reported by 1 of 2 simulators)
DataKnown_A of gen_cheriot_trvk.i_ibex_trvk.u_prim_fifo_ds_rsp_store (prim_fifo_sync.sv:224) 10 375 write responses carry the RAM's stale read data
IbexDataRPayloadX (ibex_top.sv:1527) 0 41 byte and halfword reads of partly written words
  1. IllegalParamCHERIoTNoWriteback. ibex_simple_system.sv:30 defines BASE_ISA as ibex_pkg::BaseIsaRV32IorCHERIoT
    and uses it as the default of BaseIsa; the FuseSoC define BaseIsa=ibex_pkg::BaseIsaRV32I that
    ibex_config.py passes is not used by the simple system. Configuration small sets WritebackStage=0, which
    the assertion forbids together with the CHERIoT base ISA. maxperf-pmp-bmfull (WritebackStage=1) does not
    fail. Either the simple system should take BaseIsa from the configuration, or small should not be offered with
    the CHERIoT base ISA.
  2. DataKnown_A in the TRVK downstream response FIFO. prim_ram_2p (prim_generic) updates a_rdata_o only on a
    read (a_rdata_o <= mem[a_addr_i] in the else of if (a_write_i)) and has no reset for it, so until the first
    data-side read a_rdata_o is x. The bus returns it with every write response (data_rvalid_i is 1 for writes
    too), ibex_trvk stores {data, intg, tag, err} of every response in u_prim_fifo_ds_rsp_store, and
    ASSERT_KNOWN_IF(DataKnown_A, rdata_o, rvalid_o) checks the data of write responses as well. In CoreMark the
    first data read comes at simulation time 2 447 (about cycle 1 220), after 333 write responses with all-x data;
    later write responses carry the bytes of the last read, which can be partly x (see 3). The program never uses
    that data. The check of the core itself (IbexDataRPayloadX) is qualified by is_read; the FIFO's generic
    DataKnown_A is not. Possible fixes: qualify the stored data (or the check) by "the response is to a read",
    or give the RAM's read data a known value on writes.
  3. IbexDataRPayloadX. The 41 failures are byte and halfword loads (23 with be = 0011, 18 with one byte
    enabled, from 10 words) of words whose other bytes were never written: for example address 0x001377b0 holds xxxx0066 (the lower half written by a halfword store, the upper
    half never written since the start of the simulation) and is read 22 times. The RAM returns the whole word, and
    the assertion checks all 32 bits of data_rdata_i whatever the byte enables. The loaded halfword is known, so the
    program is right. The assertion could mask the bytes that the request did not enable, or the testbench memory
    could start at a known value.

None of the three is visible in Verilator (two-state, and the simple system's Verilator build defines VERILATOR,
which empties the assertion macros).

We are happy to test a fix. This report was prepared with AI assistance (Claude Opus 5.5).

主要言語
SystemVerilog
スター
2.2k
フォーク
836
平均マージ
5日 8時間
マージ済み PR（30日）
22

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

lowRISC/ibex のほかの issue

lowRISC/ibex の issue をすべて見る

似ている issue

Embedded & IoT の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。