SymbioticEDA / riscv-formal

RISC-V Formal Verification Framework
ISC License
573 stars 94 forks source link

Support for Zce? #51

Closed Silabs-ArjanB closed 3 years ago

Silabs-ArjanB commented 3 years ago

Hi,

The proposed Zce extension has various instructions that have multiple side effects. Currently such instructions cannot be modeled with RVFI. An example are the PUSH and POP instructions, see https://github.com/riscv/riscv-code-size-reduction/blob/master/ISA%20proposals/Huawei/Zce_spec.adoc#pushpoppopret. Such instructions can perform multiple loads/stores, update multiple register file registers and optionally perform a jump.

The following could maybe all be changed into arrays to support multiple register file writes and multiple loads/stores per instruction:

output [NRET *    5 - 1 : 0] rvfi_rd_addr
output [NRET * XLEN - 1 : 0] rvfi_rd_wdata

output [NRET * XLEN   - 1 : 0] rvfi_mem_addr
output [NRET * XLEN/8 - 1 : 0] rvfi_mem_rmask
output [NRET * XLEN/8 - 1 : 0] rvfi_mem_wmask
output [NRET * XLEN   - 1 : 0] rvfi_mem_rdata
output [NRET * XLEN   - 1 : 0] rvfi_mem_wdata

Are there any plans to add assertions for Zce and for the B extension (which would require an additional register file read port)?