Skip to content

Commit

Permalink
Add RVFI signals for virtual mem instruction fetches
Browse files Browse the repository at this point in the history
Signed-off-by: Clifford Wolf <clifford@clifford.at>
  • Loading branch information
cliffordwolf committed Jan 4, 2019
1 parent 0c10bee commit e4f3400
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion docs/rvfi.md
Original file line number Diff line number Diff line change
Expand Up @@ -170,14 +170,22 @@ Alternative arithmetic operations (`RISCV_FORMAL_ALTOPS`) will be defined for al

### Modelling of Virtual Memory

For processors with support for S-mode and virtual memory we define the following additional RVFI signals:
For processors with support for S-mode and virtual memory we define the following additional RVFI signals for data load/stores:

output [NRET * 64 - 1 : 0] rvfi_mem_paddr
output [NRET * XLEN - 1 : 0] rvfi_mem_pte0
output [NRET * XLEN - 1 : 0] rvfi_mem_pte1
output [NRET * XLEN - 1 : 0] rvfi_mem_pte2
output [NRET * XLEN - 1 : 0] rvfi_mem_pte3

And the following additional RVFI signals for instruction fetches:

output [NRET * 64 - 1 : 0] rvfi_pc_paddr
output [NRET * XLEN - 1 : 0] rvfi_pc_pte0
output [NRET * XLEN - 1 : 0] rvfi_pc_pte1
output [NRET * XLEN - 1 : 0] rvfi_pc_pte2
output [NRET * XLEN - 1 : 0] rvfi_pc_pte3

And we require that the `satp` CSR is observable through RVFI:

output [NRET * XLEN - 1 : 0] rvfi_csr_satp_rmask
Expand Down

0 comments on commit e4f3400

Please sign in to comment.