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

Abierto
  • ¿Algo no está bien?
#2,577 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Los mantenedores suelen responder en 2 días

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
4/5
Tiempo estimado
3-5 días
Aptitud para principiantes
42/100
Tipo de issue
Error
Claridad
Bastante claro
Estado de actividad
Activo
Área
embedded-iot, testing

Línea de trabajo

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.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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).

Lenguaje dominante
SystemVerilog
Estrellas
2.2k
Forks
836
Merge medio
5 d 8 h
PR fusionados (30 d)
22

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de lowRISC/ibex

Todos los issues de lowRISC/ibex

Issues similares

Más issues de Embedded & IoT

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.