[Formal finding CVA6-RTL-002] Nine shipped configurations implement 8 PMP entries, a count the architecture does not permit #3575

Summary

This report concerns the frozen cva6 instance at commit 6cb200105fb9441d170e45786125a737fab98e91. The behavior below was identified by an RTL-level formal check and should be reviewed against the RISC-V specification.

Expected behavior

The implementation should satisfy the architectural requirement described by the finding title, including the stated privilege/XLEN/configuration preconditions.

Observed behavior

Nine shipped configurations implement 8 PMP entries, a count the architecture does not permit

RTL evidence

• upstream/cva6/core/include/cv64a6_imafdc_sv39_config_pkg.sv:0-0; signals: NrPMPEntries
  • NrPMPEntries = 8 in cv32a6_imac_sv32, cv64a6_imafdc_sv39, cv64a6_imafdc_sv39_hpdcache, cv64a6_imafdc_sv39_hpdcache_wb, cv64a6_imafdc_sv39_openpiton, cv64a6_imafdc_sv39_wb, cv64a6_imafdch_sv39, cv64a6_imafdch_sv39_wb and cv64a6_imafdcv_sv39. cv32a6_ima_sv32_fpga uses 0, which is permitted.
• upstream/cva6/core/csr_regfile.sv:381-382; signals: pmpcfg_o, pmpaddr_o, NrPMPEntries
  • assign pmpcfg_o = pmpcfg_q[(CVA6Cfg.NrPMPEntries>0?CVA6Cfg.NrPMPEntries-1 : 0):0]; assign pmpaddr_o = pmpaddr_q[(CVA6Cfg.NrPMPEntries>0?CVA6Cfg.NrPMPEntries-1 : 0):0];
• upstream/cva6/core/csr_regfile.sv:2922-2922; signals: NrPMPEntries
  • if (i < CVA6Cfg.NrPMPEntries) begin // the reset loop, the write logic at :2058 and the checker output are all bounded the same way

Configuration / scope

• Frozen source commit: 6cb200105fb9441d170e45786125a737fab98e91
• Repository: https://github.com/openhwfoundation/cva6
• Finding ID: CVA6-RTL-002
• Qualification status in our audit: NOT_REVALIDATED_IN_REPAIR_RUN

Reproduction

The attached evidence was obtained from the frozen RTL configuration used in our audit. A minimal reproducer should exercise the CSR/instruction/configuration named above and observe the architectural readback, trap, or state transition. The issue is intentionally reported with source locations so the behavior can be reproduced directly against the cited commit.

Request

Please confirm whether this behavior is expected for the affected configuration and, if it is a bug, advise on or provide a fix.