aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/prelude_mem.sail17
-rw-r--r--model/riscv_duopod.sail6
-rw-r--r--model/riscv_ext_regs.sail15
-rw-r--r--model/riscv_fetch.sail6
-rw-r--r--model/riscv_insts_aext.sail2
-rw-r--r--model/riscv_insts_base.sail25
-rw-r--r--model/riscv_insts_next.sail2
-rw-r--r--model/riscv_insts_zicsr.sail2
-rw-r--r--model/riscv_mem.sail71
-rw-r--r--model/riscv_platform.sail32
-rw-r--r--model/riscv_sys_control.sail12
-rw-r--r--model/riscv_sys_exceptions.sail5
-rw-r--r--model/riscv_termination_rv32.sail2
-rw-r--r--model/riscv_vmem_rv32.sail2
-rw-r--r--model/riscv_vmem_rv64.sail2
-rw-r--r--model/riscv_vmem_sv32.sail12
-rw-r--r--model/riscv_vmem_sv39.sail12
-rw-r--r--model/riscv_vmem_sv48.sail12
18 files changed, 158 insertions, 79 deletions
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index b8d47d0..85d141b 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -17,15 +17,16 @@
would be even better if it could be <= 8 bytes so that data can
also be a 64-bit int but CHERI needs 128-bit accesses for
capabilities and SIMD / vector instructions will also need more. */
- type max_mem_access : Int = 16
+type max_mem_access : Int = 16
-val write_ram : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
+val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
function write_ram(wk, addr, width, data, meta) = {
/* Write out metadata only if the value write succeeds.
* It is assumed for now that this write always succeeds;
* there is currently no return value.
- * FIXME: We should convert the external API to consume
- * the value along with the metadata to ensure atomicity.
+ * FIXME: We should convert the external API for all backends
+ * (not just for Lem) to consume the value along with the
+ * metadata to ensure atomicity.
*/
let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data);
if ret then __WriteRAM_Meta(addr, width, meta);
@@ -36,10 +37,10 @@ val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits,
function write_ram_ea(wk, addr, width) =
__write_mem_ea(wk, sizeof(xlen), addr, width)
-/* FIXME: Make this also return the metadata, which will also require external API changes. */
-val read_ram : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-function read_ram(rk, addr, width) =
- __read_mem(rk, sizeof(xlen), addr, width)
+val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt}
+function read_ram(rk, addr, width, read_meta) =
+ let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
+ (__read_mem(rk, sizeof(xlen), addr, width), meta)
val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail
index 395a332..b811824 100644
--- a/model/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
@@ -1,4 +1,6 @@
-// This file depends on the xlen definitions in riscv_xlen.sail.
+
+$include "prelude.sail"
+$include "riscv_xlen64.sail"
type regbits = bits(5)
@@ -23,7 +25,7 @@ function rX(r) =
val wX : (regbits, xlenbits) -> unit effect {wreg}
-function wX (r, v) =
+function wX(r, v) =
if r != 0b00000 then {
Xs[unsigned(r)] = v;
}
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 9ff83b3..b03ecd5 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -12,3 +12,18 @@ to omnipotent instead of null).
*/
val ext_rvfi_init : unit -> unit effect {wreg}
function ext_rvfi_init () = ()
+
+
+/*!
+THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
+at Privilege level priv. It should return true if the access is allowed.
+*/
+val ext_check_CSR : (bits(12), Privilege, bool) -> bool
+function ext_check_CSR (csrno, p, isWrite) = true
+
+/*!
+THIS is called if ext_check_CSR returns false. It should
+cause an appropriate RISCV exception.
+ */
+val ext_check_CSR_fail : unit->unit
+function ext_check_CSR_fail () = ()
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 64aff4b..cdda96e 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -4,7 +4,7 @@
function isRVC(h : half) -> bool = ~ (h[1 .. 0] == 0b11)
-val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function fetch() -> FetchResult =
/* fetch PC check for extensions: extensions return a transformed PC to fetch,
* but any exceptions use the untransformed PC.
@@ -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_insts_aext.sail b/model/riscv_insts_aext.sail
index 7eb01c5..f430a75 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -266,4 +266,4 @@ mapping amo_mnemonic : amoop <-> string = {
}
mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd)
- <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+ <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index d80d34d..bc86859 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -714,9 +714,11 @@ mapping clause encdec = MRET()
<-> 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute MRET() = {
- if cur_privilege == Machine
- then set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC))
- else handle_illegal();
+ if cur_privilege != Machine
+ then handle_illegal()
+ else if ~(ext_check_xret_priv (Machine))
+ then ext_fail_xret_priv ()
+ else set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC));
RETIRE_FAIL
}
@@ -729,15 +731,16 @@ mapping clause encdec = SRET()
<-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute SRET() = {
- match cur_privilege {
- User => handle_illegal(),
- Supervisor => if (~ (haveSupMode ())) | mstatus.TSR() == 0b1
- then handle_illegal()
- else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)),
- Machine => if (~ (haveSupMode ()))
- then handle_illegal()
- else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC))
+ let sret_illegal : bool = match cur_privilege {
+ User => true,
+ Supervisor => ~ (haveSupMode ()) | mstatus.TSR() == 0b1,
+ Machine => ~ (haveSupMode ())
};
+ if sret_illegal
+ then handle_illegal()
+ else if ~(ext_check_xret_priv (Supervisor))
+ then ext_fail_xret_priv ()
+ else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_FAIL
}
diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail
index 2af2eeb..0d23452 100644
--- a/model/riscv_insts_next.sail
+++ b/model/riscv_insts_next.sail
@@ -9,6 +9,8 @@ mapping clause encdec = URET()
function clause execute URET() = {
if (~ (haveUsrMode()))
then handle_illegal()
+ else if ~ (ext_check_xret_priv (User))
+ then ext_fail_xret_priv ()
else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC));
RETIRE_FAIL
}
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index dd8a4a0..056f537 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -179,6 +179,8 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
};
if ~ (check_CSR(csr, cur_privilege, isWrite))
then { handle_illegal(); RETIRE_FAIL }
+ else if ~ (ext_check_CSR(csr, cur_privilege, isWrite))
+ then { ext_check_CSR_fail(); RETIRE_FAIL }
else {
let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
if isWrite then {
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index d02c49d..25065ab 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -7,7 +7,7 @@
* metadata in addition to raw memory data.
*
* The external API for this module is
- * {mem_read, mem_write_ea, mem_write_value_meta, mem_write_value}
+ * {mem_read, mem_read_meta, mem_write_ea, mem_write_value_meta, mem_write_value}
* where mem_write_value is a special case of mem_write_value_meta that uses
* a default value of the metadata.
*
@@ -19,43 +19,53 @@
function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
unsigned(addr) % width == 0
-// only used for actual memory regions, to avoid MMIO effects
-function phys_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) -> MemoryOpResult(bits(8 * 'n)) = {
- let result = (match (aq, rl, res) {
- (false, false, false) => Some(read_ram(Read_plain, paddr, width)),
- (true, false, false) => Some(read_ram(Read_RISCV_acquire, paddr, width)),
- (true, true, false) => Some(read_ram(Read_RISCV_strong_acquire, paddr, width)),
- (false, false, true) => Some(read_ram(Read_RISCV_reserved, paddr, width)),
- (true, false, true) => Some(read_ram(Read_RISCV_reserved_acquire, paddr, width)),
- (true, true, true) => Some(read_ram(Read_RISCV_reserved_strong_acquire, paddr, width)),
+function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) =
+ match (aq, rl, res) {
+ (false, false, false) => Some(Read_plain),
+ (true, false, false) => Some(Read_RISCV_acquire),
+ (true, true, false) => Some(Read_RISCV_strong_acquire),
+ (false, false, true) => Some(Read_RISCV_reserved),
+ (true, false, true) => Some(Read_RISCV_reserved_acquire),
+ (true, true, true) => Some(Read_RISCV_reserved_strong_acquire),
(false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */
(false, true, true) => None()
- }) : option(bits(8 * 'n));
+ }
+
+// only used for actual memory regions, to avoid MMIO effects
+function phys_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)) = {
+ let result = (match read_kind_of_flags(aq, rl, res) {
+ Some(rk) => Some(read_ram(rk, paddr, width, meta)),
+ None() => None()
+ }) : option((bits(8 * 'n), mem_meta));
match (t, result) {
(Execute(), None()) => MemException(E_Fetch_Access_Fault()),
(Read(Data), None()) => MemException(E_Load_Access_Fault()),
(_, None()) => MemException(E_SAMO_Access_Fault()),
- (_, Some(v)) => { if get_config_print_mem()
+ (_, Some(v, m)) => { if get_config_print_mem()
then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v));
- MemValue(v) }
+ MemValue(v, m) }
}
}
/* 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) -> MemoryOpResult(bits(8 * 'n)) =
+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 mmio_read(paddr, width)
+ 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)
- else MemException(E_Load_Access_Fault())
+ then phys_mem_read(t, paddr, width, aq, rl, res, meta)
+ 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) -> MemoryOpResult(bits(8 * 'n)) =
+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)) =
if (~ (plat_enable_pmp ()))
- then checked_mem_read(t, paddr, width, aq, rl, res)
+ then checked_mem_read(t, paddr, width, aq, rl, res, meta)
else {
match pmpCheck(paddr, width, t, effectivePrivilege(mstatus, cur_privilege)) {
- None() => checked_mem_read(t, paddr, width, aq, rl, res),
+ None() => checked_mem_read(t, paddr, width, aq, rl, res, meta),
Some(e) => MemException(e)
}
}
@@ -81,9 +91,11 @@ $endif
/* NOTE: The rreg effect is due to MMIO. */
$ifdef RVFI_DII
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
$else
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
$endif
function mem_read (typ, paddr, width, aq, rl, res) = {
@@ -93,12 +105,25 @@ function mem_read (typ, paddr, width, aq, rl, res) = {
else match (aq, rl, res) {
(false, true, false) => throw(Error_not_implemented("load.rl")),
(false, true, true) => throw(Error_not_implemented("lr.rl")),
- (_, _, _) => pmp_mem_read(typ, paddr, width, aq, rl, res)
+ (_, _, _) => MemoryOpResult_drop_meta(pmp_mem_read(typ, paddr, width, aq, rl, res, false))
};
rvfi_read(paddr, width, result);
result
}
+function mem_read_meta (typ, addr, width, aq, rl, res) = {
+ let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
+ if (aq | res) & (~ (is_aligned_addr(addr, width)))
+ then MemException(E_Load_Addr_Align())
+ else match (aq, rl, res) {
+ (false, true, false) => throw(Error_not_implemented("load.rl")),
+ (false, true, true) => throw(Error_not_implemented("lr.rl")),
+ (_, _, _) => pmp_mem_read(typ, addr, width, aq, rl, res, true)
+ };
+ rvfi_read(addr, width, MemoryOpResult_drop_meta(result));
+ result
+}
+
val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
function mem_write_ea (addr, width, aq, rl, con) = {
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)
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 2886273..d906f5e 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -497,3 +497,15 @@ union MemoryOpResult ('a : Type) = {
MemValue : 'a,
MemException : ExceptionType
}
+
+val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta))
+function MemoryOpResult_add_meta(r, m) = match r {
+ MemValue(v) => MemValue(v, m),
+ MemException(e) => MemException(e)
+}
+
+val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t)
+function MemoryOpResult_drop_meta(r) = match r {
+ MemValue(v, m) => MemValue(v),
+ MemException(e) => MemException(e)
+}
diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail
index 94d869e..fa693e8 100644
--- a/model/riscv_sys_exceptions.sail
+++ b/model/riscv_sys_exceptions.sail
@@ -2,6 +2,11 @@
type ext_exception = unit
+/* Is XRET from given mode permitted by extension? */
+function ext_check_xret_priv (p : Privilege) : Privilege -> bool = true
+/* Called if above check fails */
+function ext_fail_xret_priv () : unit -> unit = ()
+
function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -> unit = ()
/* used for traps and ECALL */
diff --git a/model/riscv_termination_rv32.sail b/model/riscv_termination_rv32.sail
index 7cf8cb8..7318421 100644
--- a/model/riscv_termination_rv32.sail
+++ b/model/riscv_termination_rv32.sail
@@ -1 +1 @@
-termination_measure walk32(_,_,_,_,_,_,level,_) = level
+termination_measure walk32(_,_,_,_,_,_,level,_,_) = level
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index 4ff7891..bea786c 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -26,7 +26,7 @@ function translationMode(priv) = {
/* Top-level address translation dispatcher */
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function translateAddr(vAddr, ac) = {
let effPriv : Privilege = match ac {
Execute() => cur_privilege,
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index c55e9dc..8b7dc44 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -33,7 +33,7 @@ function translationMode(priv) = {
/* Top-level address translation dispatcher */
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function translateAddr(vAddr, ac) = {
let effPriv : Privilege = match ac {
Execute() => cur_privilege,
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index e535915..1a27072 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -6,7 +6,7 @@
function to_phys_addr(a : paddr32) -> xlenbits = a[31..0]
-val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rreg, escape}
+val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rmemt, rreg, escape}
function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
let va = Mk_SV32_Vaddr(vaddr);
let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]),
@@ -37,13 +37,13 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
if isPTEPtr(pbits, ext_pte) then {
- if level == 0 then {
+ if level > 0 then {
+ /* walk down the pointer to the next level */
+ walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
+ } else {
/* last-level PTE contains a pointer instead of a leaf */
/* print("walk32: last-level pte contains a ptr"); */
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- } else {
- /* walk down the pointer to the next level */
- walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
}
} else { /* leaf PTE */
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
@@ -115,7 +115,7 @@ function flush_TLB32(asid, addr) =
/* address translation */
-val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
match lookup_TLB32(asid, vAddr) {
Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a1edc4e..37c98a2 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -1,6 +1,6 @@
/* Sv39 address translation for RV64. */
-val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rreg, escape}
+val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rmemt, rreg, escape}
function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
let va = Mk_SV39_Vaddr(vaddr);
let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
@@ -31,13 +31,13 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
if isPTEPtr(pbits, ext_pte) then {
- if level == 0 then {
+ if level > 0 then {
+ /* walk down the pointer to the next level */
+ walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
+ } else {
/* last-level PTE contains a pointer instead of a leaf */
/* print("walk39: last-level pte contains a ptr"); */
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- } else {
- /* walk down the pointer to the next level */
- walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
}
} else { /* leaf PTE */
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
@@ -109,7 +109,7 @@ function flush_TLB39(asid, addr) =
/* address translation */
-val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
match lookup_TLB39(asid, vAddr) {
Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 6bfeea4..36304cf 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -1,6 +1,6 @@
/* Sv48 address translation for RV64. */
-val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape}
+val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rmemt, rreg, escape}
function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
let va = Mk_SV48_Vaddr(vaddr);
let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
@@ -31,13 +31,13 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
if isPTEPtr(pbits, ext_pte) then {
- if level == 0 then {
+ if level > 0 then {
+ /* walk down the pointer to the next level */
+ walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
+ } else {
/* last-level PTE contains a pointer instead of a leaf */
/* print("walk48: last-level pte contains a ptr"); */
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- } else {
- /* walk down the pointer to the next level */
- walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
}
} else { /* leaf PTE */
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
@@ -109,7 +109,7 @@ function flush_TLB48(asid, addr) =
/* address translation */
-val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {
PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
generated by cgit v1.1 at 2024-11-06 02:23:12 +0000