aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Norton <rmn30@cam.ac.uk>2019-07-17 13:44:30 +0100
committerRobert Norton <rmn30@cam.ac.uk>2019-07-17 13:44:30 +0100
commit8c8bef62070fa4ef22422f89d684fd6b1adaa38a (patch)
tree6247133961cbe894f64e789e140b5f7737713f66
parent8b39adca2fafad9037f21202782ac29c776b7526 (diff)
downloadsail-riscv-8c8bef62070fa4ef22422f89d684fd6b1adaa38a.zip
sail-riscv-8c8bef62070fa4ef22422f89d684fd6b1adaa38a.tar.gz
sail-riscv-8c8bef62070fa4ef22422f89d684fd6b1adaa38a.tar.bz2
Disable mmio devices (clint and htif interfaces) when using RVFI to prevent divergence when using TestRIG.
-rw-r--r--model/riscv_platform.sail9
1 files changed, 8 insertions, 1 deletions
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 9184f02..52511a9 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -337,12 +337,19 @@ function htif_tick() = {
}
/* Top-level MMIO dispatch */
-
+$ifndef RVFI_DII
function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool =
within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n)
+$else
+function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
+$endif
+$ifndef RVFI_DII
function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool =
within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
+$else
+function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
+$endif
function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
if within_clint(addr, width)