aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPrashanth Mundkur <prashanth.mundkur@gmail.com>2020-01-06 12:08:49 -0800
committerGitHub <noreply@github.com>2020-01-06 12:08:49 -0800
commit4327e878eafb308e735cd2354265b39b190a6dca (patch)
tree16e47d7768f4ea2546f9e1279f552264f3086f1c
parentae655e7d45bc9ff245ae907683298f4119908d71 (diff)
parentdd0f51d1d681b92348e56abe2e20aac11dfda130 (diff)
downloadsail-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.sail4
-rw-r--r--model/riscv_mem.sail8
-rw-r--r--model/riscv_platform.sail32
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)