diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-06 12:08:49 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-06 12:08:49 -0800 |
commit | 4327e878eafb308e735cd2354265b39b190a6dca (patch) | |
tree | 16e47d7768f4ea2546f9e1279f552264f3086f1c | |
parent | ae655e7d45bc9ff245ae907683298f4119908d71 (diff) | |
parent | dd0f51d1d681b92348e56abe2e20aac11dfda130 (diff) | |
download | sail-riscv-4327e878eafb308e735cd2354265b39b190a6dca.zip sail-riscv-4327e878eafb308e735cd2354265b39b190a6dca.tar.gz sail-riscv-4327e878eafb308e735cd2354265b39b190a6dca.tar.bz2 |
Merge pull request #30 from jrtc27/amo-fault
Generate correct cause for AMO faults
-rw-r--r-- | model/riscv_fetch.sail | 4 | ||||
-rw-r--r-- | model/riscv_mem.sail | 8 | ||||
-rw-r--r-- | model/riscv_platform.sail | 32 |
3 files changed, 30 insertions, 14 deletions
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index d091756..cdda96e 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -22,7 +22,7 @@ function fetch() -> FetchResult = * exceptions. */ match mem_read(Execute(), ppclo, 2, false, false, false) { - MemException(e) => F_Error(E_Fetch_Access_Fault(), PC), + MemException(e) => F_Error(e, PC), MemValue(ilo) => { if isRVC(ilo) then F_RVC(ilo) @@ -36,7 +36,7 @@ function fetch() -> FetchResult = TR_Failure(e, _) => F_Error(e, PC_hi), TR_Address(ppchi, _) => { match mem_read(Execute(), ppchi, 2, false, false, false) { - MemException(e) => F_Error(E_Fetch_Access_Fault(), PC_hi), + MemException(e) => F_Error(e, PC_hi), MemValue(ihi) => F_Base(append(ihi, ilo)) } } diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 3fd6f31..25065ab 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -50,10 +50,14 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = if within_mmio_readable(paddr, width) - then MemoryOpResult_add_meta(mmio_read(paddr, width), default_meta) + then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta) else if within_phys_mem(paddr, width) then phys_mem_read(t, paddr, width, aq, rl, res, meta) - else MemException(E_Load_Access_Fault()) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } /* PMP checks if enabled */ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 7cc63cc..7e07cf1 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -142,8 +142,8 @@ let MTIMECMP_BASE_HI : xlenbits = EXTZ(0x04004) let MTIME_BASE : xlenbits = EXTZ(0x0bff8) let MTIME_BASE_HI : xlenbits = EXTZ(0x0bffc) -val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function clint_load(addr, width) = { +val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function clint_load(t, addr, width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ if addr == MSIP_BASE & ('n == 8 | 'n == 4) @@ -194,7 +194,11 @@ function clint_load(addr, width) = { else { if get_config_print_platform() then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>"); - MemException(E_Load_Access_Fault()) + match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } } @@ -274,8 +278,8 @@ register htif_exit_code : bits(64) * dispatched the address. */ -val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function htif_load(paddr, width) = { +val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function htif_load(t, paddr, width) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ @@ -285,7 +289,11 @@ function htif_load(paddr, width) = { then MemValue(sail_zero_extend(htif_tohost[31..0], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ else if width == 4 & paddr == plat_htif_tohost() + 4 then MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else MemException(E_Load_Access_Fault()) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ @@ -351,12 +359,16 @@ $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 . (paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = +function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) - then clint_load(paddr, width) + then clint_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) - then htif_load(paddr, width) - else MemException(E_Load_Access_Fault()) + then htif_load(t, paddr, width) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_clint(paddr, width) |