aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/riscv_addr_checks.sail2
-rw-r--r--model/riscv_fetch.sail8
-rw-r--r--model/riscv_insts_aext.sail22
-rw-r--r--model/riscv_insts_base.sail16
-rw-r--r--model/riscv_mem.sail44
-rw-r--r--model/riscv_pmp_control.sail24
-rw-r--r--model/riscv_pte.sail50
-rw-r--r--model/riscv_ptw.sail37
-rw-r--r--model/riscv_types.sail18
-rw-r--r--model/riscv_vmem_common.sail89
-rw-r--r--model/riscv_vmem_rv64.sail6
-rw-r--r--model/riscv_vmem_sv39.sail4
-rw-r--r--model/riscv_vmem_sv48.sail4
-rw-r--r--model/riscv_vmem_types.sail18
14 files changed, 176 insertions, 166 deletions
diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index 06e20f9..318d2a2 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -46,7 +46,7 @@ type ext_data_addr_error = unit
/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
-function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType, width : word_width)
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index ae8748c..d615691 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -14,14 +14,14 @@ function fetch() -> FetchResult =
Ext_FetchAddr_OK(use_pc) => {
if (use_pc[0] != 0b0 | (use_pc[1] != 0b0 & (~ (haveRVC()))))
then F_Error(E_Fetch_Addr_Align, PC)
- else match translateAddr(use_pc, Execute) {
+ else match translateAddr(use_pc, Execute()) {
TR_Failure(e) => F_Error(e, PC),
TR_Address(ppclo) => {
/* split instruction fetch into 16-bit granules to handle RVC, as
* well as to generate precise fault addresses in any fetch
* exceptions.
*/
- match mem_read(Execute, ppclo, 2, false, false, false) {
+ match mem_read(Execute(), ppclo, 2, false, false, false) {
MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
MemValue(ilo) => {
if isRVC(ilo)
@@ -32,10 +32,10 @@ function fetch() -> FetchResult =
match ext_fetch_check_pc(PC, PC_hi) {
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc_hi) => {
- match translateAddr(use_pc_hi, Execute) {
+ match translateAddr(use_pc_hi, Execute()) {
TR_Failure(e) => F_Error(e, PC_hi),
TR_Address(ppchi) => {
- match mem_read(Execute, ppchi, 2, false, false, false) {
+ match mem_read(Execute(), ppchi, 2, false, false, false) {
MemException(e) => F_Error(E_Fetch_Access_Fault, PC_hi),
MemValue(ihi) => F_Base(append(ihi, ilo))
}
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index cd2f069..a9d6be7 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -44,7 +44,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
- match ext_data_get_addr(rs1, zeros(), Read, width) {
+ match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
@@ -62,12 +62,12 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
*/
if (~ (aligned))
then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
- else match translateAddr(vaddr, Read) {
+ else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) =>
match (width, sizeof(xlen)) {
- (WORD, _) => process_loadres(rd, vaddr, mem_read(Read, addr, 4, aq, rl, true), false),
- (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read, addr, 8, aq, rl, true), false),
+ (WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, true), false),
+ (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, true), false),
_ => internal_error("LOADRES expected WORD or DOUBLE")
}
}
@@ -103,7 +103,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
- match ext_data_get_addr(rs1, zeros(), Write, width) {
+ match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
@@ -123,8 +123,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* cannot happen in rmem */
X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS
} else {
- match translateAddr(vaddr, Write) { /* Write and ReadWrite are equivalent here:
- * both result in a SAMO exception */
+ match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
+ * both result in a SAMO exception */
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -189,10 +189,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
- match ext_data_get_addr(rs1, zeros(), ReadWrite, width) {
+ match ext_data_get_addr(rs1, zeros(), ReadWrite(Data), width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
- match translateAddr(vaddr, ReadWrite) {
+ match translateAddr(vaddr, ReadWrite(Data)) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -205,8 +205,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
MemValue(_) => {
let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
- (WORD, _) => extend_value(false, mem_read(ReadWrite, addr, 4, aq, aq & rl, true)),
- (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite, addr, 8, aq, aq & rl, true)),
+ (WORD, _) => extend_value(false, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
+ (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)),
_ => internal_error ("AMO expected WORD or DOUBLE")
};
match (rval) {
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 14a626e..0df5ce8 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -318,23 +318,23 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
- match ext_data_get_addr(rs1, offset, Read, width) {
+ match ext_data_get_addr(rs1, offset, Read(Data), width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
- else match translateAddr(vaddr, Read) {
+ else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) =>
match (width, sizeof(xlen)) {
(BYTE, _) =>
- process_load(rd, vaddr, mem_read(Read, addr, 1, aq, rl, false), is_unsigned),
+ process_load(rd, vaddr, mem_read(Read(Data), addr, 1, aq, rl, false), is_unsigned),
(HALF, _) =>
- process_load(rd, vaddr, mem_read(Read, addr, 2, aq, rl, false), is_unsigned),
+ process_load(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, false), is_unsigned),
(WORD, _) =>
- process_load(rd, vaddr, mem_read(Read, addr, 4, aq, rl, false), is_unsigned),
+ process_load(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, false), is_unsigned),
(DOUBLE, 64) =>
- process_load(rd, vaddr, mem_read(Read, addr, 8, aq, rl, false), is_unsigned)
+ process_load(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, false), is_unsigned)
}
}
}
@@ -373,12 +373,12 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
- match ext_data_get_addr(rs1, offset, Write, width) {
+ match ext_data_get_addr(rs1, offset, Write(Data), width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
- else match translateAddr(vaddr, Write) {
+ else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) => {
let eares : MemoryOpResult(unit) = match width {
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 9f417c0..b62caf8 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -20,7 +20,7 @@ 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, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
+function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : 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, addr, width)),
(true, false, false) => Some(read_ram(Read_RISCV_acquire, addr, width)),
@@ -32,17 +32,17 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, ad
(false, true, true) => None()
}) : option(bits(8 * 'n));
match (t, result) {
- (Execute, None()) => MemException(E_Fetch_Access_Fault),
- (Read, None()) => MemException(E_Load_Access_Fault),
- (_, None()) => MemException(E_SAMO_Access_Fault),
- (_, Some(v)) => { if get_config_print_mem()
- then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
- MemValue(v) }
+ (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()
+ then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+ MemValue(v) }
}
}
/* 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, addr : 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), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
if within_mmio_readable(addr, width)
then mmio_read(addr, width)
else if within_phys_mem(addr, width)
@@ -50,7 +50,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType,
else MemException(E_Load_Access_Fault)
/* PMP checks if enabled */
-function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : 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), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
if (~ (plat_enable_pmp ()))
then checked_mem_read(t, addr, width, aq, rl, res)
else {
@@ -81,9 +81,9 @@ $endif
/* NOTE: The rreg effect is due to MMIO. */
$ifdef RVFI_DII
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType, 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, rreg, escape}
$else
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType, 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, rreg, escape}
$endif
function mem_read (typ, addr, width, aq, rl, res) = {
@@ -148,10 +148,10 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
else MemException(E_SAMO_Access_Fault)
/* PMP checks if enabled */
-function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) =
+function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) =
if (~ (plat_enable_pmp ()))
then checked_mem_write(wk, addr, width, data, meta)
- else match pmpCheck(addr, width, Write, effectivePrivilege(mstatus, cur_privilege)) {
+ else match pmpCheck(addr, width, Write(ext_acc), effectivePrivilege(mstatus, cur_privilege)) {
None() => checked_mem_write(wk, addr, width, data, meta),
Some(e) => MemException(e)
}
@@ -163,18 +163,18 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, ad
* data.
* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime.
*/
-val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
-function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = {
+val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) = {
rvfi_write(addr, width, value);
if (rl | con) & (~ (is_aligned_addr(addr, width)))
then MemException(E_SAMO_Addr_Align)
else match (aq, rl, con) {
- (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, meta),
- (false, true, false) => pmp_mem_write(Write_RISCV_release, addr, width, value, meta),
- (false, false, true) => pmp_mem_write(Write_RISCV_conditional, addr, width, value, meta),
- (false, true , true) => pmp_mem_write(Write_RISCV_conditional_release, addr, width, value, meta),
- (true, true, false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, meta),
- (true, true , true) => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, meta),
+ (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, ext_acc, meta),
+ (false, true, false) => pmp_mem_write(Write_RISCV_release, addr, width, value, ext_acc, meta),
+ (false, false, true) => pmp_mem_write(Write_RISCV_conditional, addr, width, value, ext_acc, meta),
+ (false, true , true) => pmp_mem_write(Write_RISCV_conditional_release, addr, width, value, ext_acc, meta),
+ (true, true, false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, ext_acc, meta),
+ (true, true , true) => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, ext_acc, meta),
// throw an illegal instruction here?
(true, false, false) => throw(Error_not_implemented("store.aq")),
(true, false, true) => throw(Error_not_implemented("sc.aq"))
@@ -184,4 +184,4 @@ function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = {
/* Memory write with a default metadata value. */
val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
function mem_write_value (addr, width, value, aq, rl, con) =
- mem_write_value_meta(addr, width, value, default_meta, aq, rl, con)
+ mem_write_value_meta(addr, width, value, default_write_acc, default_meta, aq, rl, con)
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 4c65f7d..c1de35c 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -26,18 +26,18 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
/* permission checks */
-val pmpCheckRWX: (Pmpcfg_ent, AccessType) -> bool
+val pmpCheckRWX: (Pmpcfg_ent, AccessType(ext_access_type)) -> bool
function pmpCheckRWX(ent, acc) = {
match acc {
- Read => ent.R() == true,
- Write => ent.W() == true,
- ReadWrite => ent.R() == true & ent.W() == true,
- Execute => ent.X() == true
+ Read(Data) => ent.R() == true,
+ Write(Data) => ent.W() == true,
+ ReadWrite(Data) => ent.R() == true & ent.W() == true,
+ Execute() => ent.X() == true
}
}
// this needs to be called with the effective current privilege.
-val pmpCheckPerms: (Pmpcfg_ent, AccessType, Privilege) -> bool
+val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
function pmpCheckPerms(ent, acc, priv) = {
match priv {
Machine => if ent.L() == true
@@ -68,7 +68,7 @@ function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> p
enum pmpMatch = {PMP_Success, PMP_Continue, PMP_Fail}
-function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privilege,
+function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege,
ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmpMatch = {
let rng = pmpAddrRange(ent, pmpaddr, prev_pmpaddr);
match pmpMatchAddr(addr, width, rng) {
@@ -82,7 +82,7 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: P
/* priority checks */
-function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType, priv: Privilege)
+function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
let check : bool =
@@ -158,10 +158,10 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
if check
then None()
else match acc {
- Read => Some(E_Load_Access_Fault),
- Write => Some(E_SAMO_Access_Fault),
- ReadWrite => Some(E_SAMO_Access_Fault),
- Execute => Some(E_Fetch_Access_Fault)
+ Read(Data) => Some(E_Load_Access_Fault),
+ Write(Data) => Some(E_SAMO_Access_Fault),
+ ReadWrite(Data) => Some(E_SAMO_Access_Fault),
+ Execute() => Some(E_Fetch_Access_Fault)
}
}
diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
new file mode 100644
index 0000000..34266cc
--- /dev/null
+++ b/model/riscv_pte.sail
@@ -0,0 +1,50 @@
+/* PTE attributes, permission checks and updates */
+
+type pteAttribs = bits(8)
+
+bitfield PTE_Bits : pteAttribs = {
+ D : 7,
+ A : 6,
+ G : 5,
+ U : 4,
+ X : 3,
+ W : 2,
+ R : 1,
+ V : 0
+}
+
+function isPTEPtr(p : pteAttribs) -> bool = {
+ let a = Mk_PTE_Bits(p);
+ a.R() == false & a.W() == false & a.X() == false
+}
+
+function isInvalidPTE(p : pteAttribs) -> bool = {
+ let a = Mk_PTE_Bits(p);
+ a.V() == false | (a.W() == true & a.R() == false)
+}
+
+function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = {
+ match (ac, priv) {
+ (Read(Data), User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
+ (Write(Data), User) => p.U() == true & p.W() == true,
+ (ReadWrite(Data), User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
+ (Execute(), User) => p.U() == true & p.X() == true,
+
+ (Read(Data), Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
+ (Write(Data), Supervisor) => (p.U() == false | do_sum) & p.W() == true,
+ (ReadWrite(Data), Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
+ (Execute(), Supervisor) => p.U() == false & p.X() == true,
+
+ (_, Machine) => internal_error("m-mode mem perm check")
+ }
+}
+
+function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type)) -> option(PTE_Bits) = {
+ let update_d = (a == Write(Data) | a == ReadWrite(Data)) & p.D() == false; // dirty-bit
+ let update_a = p.A() == false; // accessed-bit
+ if update_d | update_a then {
+ let np = update_A(p, true);
+ let np = if update_d then update_D(np, true) else np;
+ Some(np)
+ } else None()
+}
diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail
new file mode 100644
index 0000000..e2056b4
--- /dev/null
+++ b/model/riscv_ptw.sail
@@ -0,0 +1,37 @@
+/* failure modes for address-translation/page-table-walks */
+enum PTW_Error = {
+ PTW_Access, /* physical memory access error for a PTE */
+ PTW_Invalid_PTE,
+ PTW_No_Permission,
+ PTW_Misaligned, /* misaligned superpage */
+ PTW_PTE_Update /* PTE update needed but not enabled */
+}
+val ptw_error_to_str : PTW_Error -> string
+function ptw_error_to_str(e) =
+ match (e) {
+ PTW_Access => "mem-access-error",
+ PTW_Invalid_PTE => "invalid-pte",
+ PTW_No_Permission => "no-permission",
+ PTW_Misaligned => "misaligned-superpage",
+ PTW_PTE_Update => "pte-update-needed"
+ }
+
+overload to_str = {ptw_error_to_str}
+
+/* conversion of these translation/PTW failures into architectural exceptions */
+function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = {
+ let e : ExceptionType =
+ match (a, f) {
+ (ReadWrite(Data), PTW_Access) => E_SAMO_Access_Fault,
+ (ReadWrite(Data), _) => E_SAMO_Page_Fault,
+ (Read(Data), PTW_Access) => E_Load_Access_Fault,
+ (Read(Data), _) => E_Load_Page_Fault,
+ (Write(Data), PTW_Access) => E_SAMO_Access_Fault,
+ (Write(Data), _) => E_SAMO_Page_Fault,
+ (Execute(), PTW_Access) => E_Fetch_Access_Fault,
+ (Execute(), _) => E_Fetch_Page_Fault
+ } in {
+/* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
+ e
+ }
+}
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index a47afc3..e0a1f45 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -97,18 +97,12 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
/* memory access types */
-enum AccessType = {Read, Write, ReadWrite, Execute}
-
-val accessType_to_str : AccessType -> string
-function accessType_to_str (a) =
- match (a) {
- Read => "R",
- Write => "W",
- ReadWrite => "RW",
- Execute => "X"
- }
-
-overload to_str = {accessType_to_str}
+union AccessType ('a : Type) = {
+ Read : 'a,
+ Write : 'a,
+ ReadWrite : 'a,
+ Execute : unit
+}
enum word_width = {BYTE, HALF, WORD, DOUBLE}
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index c8808f7..f77366b 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -8,95 +8,6 @@
let PAGESIZE_BITS = 12
-/* PTE attributes, permission checks and updates */
-
-type pteAttribs = bits(8)
-
-bitfield PTE_Bits : pteAttribs = {
- D : 7,
- A : 6,
- G : 5,
- U : 4,
- X : 3,
- W : 2,
- R : 1,
- V : 0
-}
-
-function isPTEPtr(p : pteAttribs) -> bool = {
- let a = Mk_PTE_Bits(p);
- a.R() == false & a.W() == false & a.X() == false
-}
-
-function isInvalidPTE(p : pteAttribs) -> bool = {
- let a = Mk_PTE_Bits(p);
- a.V() == false | (a.W() == true & a.R() == false)
-}
-
-function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = {
- match (ac, priv) {
- (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
- (Write, User) => p.U() == true & p.W() == true,
- (ReadWrite, User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
- (Execute, User) => p.U() == true & p.X() == true,
-
- (Read, Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
- (Write, Supervisor) => (p.U() == false | do_sum) & p.W() == true,
- (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
- (Execute, Supervisor) => p.U() == false & p.X() == true,
-
- (_, Machine) => internal_error("m-mode mem perm check")
- }
-}
-
-function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = {
- let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit
- let update_a = p.A() == false; // accessed-bit
- if update_d | update_a then {
- let np = update_A(p, true);
- let np = if update_d then update_D(np, true) else np;
- Some(np)
- } else None()
-}
-
-/* failure modes for address-translation/page-table-walks */
-enum PTW_Error = {
- PTW_Access, /* physical memory access error for a PTE */
- PTW_Invalid_PTE,
- PTW_No_Permission,
- PTW_Misaligned, /* misaligned superpage */
- PTW_PTE_Update /* PTE update needed but not enabled */
-}
-val ptw_error_to_str : PTW_Error -> string
-function ptw_error_to_str(e) =
- match (e) {
- PTW_Access => "mem-access-error",
- PTW_Invalid_PTE => "invalid-pte",
- PTW_No_Permission => "no-permission",
- PTW_Misaligned => "misaligned-superpage",
- PTW_PTE_Update => "pte-update-needed"
- }
-
-overload to_str = {ptw_error_to_str}
-
-/* conversion of these translation/PTW failures into architectural exceptions */
-function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = {
- let e : ExceptionType =
- match (a, f) {
- (ReadWrite, PTW_Access) => E_SAMO_Access_Fault,
- (ReadWrite, _) => E_SAMO_Page_Fault,
- (Read, PTW_Access) => E_Load_Access_Fault,
- (Read, _) => E_Load_Page_Fault,
- (Write, PTW_Access) => E_SAMO_Access_Fault,
- (Write, _) => E_SAMO_Page_Fault,
- (Fetch, PTW_Access) => E_Fetch_Access_Fault,
- (Fetch, _) => E_Fetch_Page_Fault
- } in {
-/* print("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
- e
- }
-}
-
/*
* Definitions for RV32, which has a single address translation mode: Sv32.
*/
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index e3cca0b..467ac5f 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -33,11 +33,11 @@ function translationMode(priv) = {
/* Top-level address translation dispatcher */
-val translateAddr : (xlenbits, AccessType) -> 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, rreg, wmv, wmvt, wreg}
function translateAddr(vAddr, ac) = {
let effPriv : Privilege = match ac {
- Execute => cur_privilege,
- _ => effectivePrivilege(mstatus, cur_privilege)
+ Execute() => cur_privilege,
+ _ => effectivePrivilege(mstatus, cur_privilege)
};
let mxr : bool = mstatus.MXR() == true;
let do_sum : bool = mstatus.SUM() == true;
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a575a07..c31a9bb 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, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rreg, escape}
+val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rreg, escape}
function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let va = Mk_SV39_Vaddr(vaddr);
let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
@@ -105,7 +105,7 @@ function flush_TLB39(asid, addr) =
/* address translation */
-val translate39 : (asid64, paddr64, vaddr39, AccessType, Privilege, bool, bool, nat) -> 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) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
match lookup_TLB39(asid, vAddr) {
Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index a898ac7..664807c 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, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape}
+val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape}
function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let va = Mk_SV48_Vaddr(vaddr);
let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
@@ -105,7 +105,7 @@ function flush_TLB48(asid, addr) =
/* address translation */
-val translate48 : (asid64, paddr64, vaddr48, AccessType, Privilege, bool, bool, nat) -> 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) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false) {
PTW_Failure(f) => TR_Failure(f),
diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail
new file mode 100644
index 0000000..577de37
--- /dev/null
+++ b/model/riscv_vmem_types.sail
@@ -0,0 +1,18 @@
+// Specialize the accesstype for memory
+
+type ext_access_type = unit
+
+let Data : ext_access_type = ()
+
+let default_write_acc : ext_access_type = Data
+
+val accessType_to_str : AccessType(ext_access_type) -> string
+function accessType_to_str (a) =
+ match (a) {
+ Read(Data) => "R",
+ Write(Data) => "W",
+ ReadWrite(Data) => "RW",
+ Execute() => "X"
+ }
+
+overload to_str = {accessType_to_str}
generated by cgit v1.1 at 2024-11-06 00:53:50 +0000