diff options
-rw-r--r-- | Makefile | 28 | ||||
-rw-r--r-- | handwritten_support/0.11/mem_metadata.lem | 16 | ||||
-rw-r--r-- | handwritten_support/mem_metadata.lem | 16 | ||||
-rw-r--r-- | model/prelude_mem.sail | 17 | ||||
-rw-r--r-- | model/riscv_fetch.sail | 2 | ||||
-rw-r--r-- | model/riscv_mem.sail | 65 | ||||
-rw-r--r-- | model/riscv_sys_control.sail | 12 | ||||
-rw-r--r-- | model/riscv_vmem_rv64.sail | 2 | ||||
-rw-r--r-- | model/riscv_vmem_sv39.sail | 4 | ||||
-rw-r--r-- | model/riscv_vmem_sv48.sail | 4 |
10 files changed, 114 insertions, 52 deletions
@@ -129,14 +129,15 @@ else C_FLAGS += -O3 -flto endif +RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem # Feature detect if we are on the latest development version of Sail # and use an updated lem file if so. This is just until the opam # version catches up with changes to the barrier type. SAIL_LATEST := $(shell $(SAIL) -have_feature FEATURE_UNION_BARRIER 1>&2 2> /dev/null; echo $$?) ifeq ($(SAIL_LATEST),0) -RISCV_EXTRAS_LEM = 0.11/riscv_extras.lem +RISCV_EXTRAS_LEM = $(addprefix handwritten_support/0.11/,$(RISCV_EXTRAS_LEM_FILES)) else -RISCV_EXTRAS_LEM = riscv_extras.lem +RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) endif all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem @@ -221,10 +222,10 @@ generated_definitions/isabelle/$(ARCH)/ROOT: handwritten_support/ROOT generated_definitions/lem/riscv_duopod.lem: $(PRELUDE_SRCS) model/riscv_duopod.sail mkdir -p generated_definitions/lem - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ -generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv_duopod.lem handwritten_support/$(RISCV_EXTRAS_LEM) + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -lem_mwords -lem_lib Riscv_extras -lem_lib Mem_metadata -o riscv_duopod $^ +generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv_duopod.lem $(RISCV_EXTRAS_LEM) lem -isa -outdir generated_definitions/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - handwritten_support/$(RISCV_EXTRAS_LEM) \ + $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/riscv_duopod_types.lem \ generated_definitions/lem/riscv_duopod.lem @@ -244,17 +245,12 @@ endif generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Mem_metadata $(SAIL_SRCS) echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem -generated_definitions/lem/$(ARCH)/riscv_sequential.lem: $(SAIL_SRCS) Makefile - mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) - $(SAIL_DIR)/sail -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) - echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem - -generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) Makefile +generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - handwritten_support/$(RISCV_EXTRAS_LEM) \ + $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/$(ARCH)/riscv_types.lem \ generated_definitions/lem/$(ARCH)/riscv.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/$(ARCH)/Riscv_types.thy @@ -264,10 +260,10 @@ generated_definitions/hol4/$(ARCH)/Holmakefile: handwritten_support/Holmakefile mkdir -p generated_definitions/hol4/$(ARCH) cp handwritten_support/Holmakefile generated_definitions/hol4/$(ARCH) -generated_definitions/hol4/$(ARCH)/riscvScript.sml: generated_definitions/hol4/$(ARCH)/Holmakefile generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) +generated_definitions/hol4/$(ARCH)/riscvScript.sml: generated_definitions/hol4/$(ARCH)/Holmakefile generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) lem -hol -outdir generated_definitions/hol4/$(ARCH) -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ -lib $(SAIL_DIR)/src/lem_interp -lib $(SAIL_DIR)/src/gen_lib \ - handwritten_support/$(RISCV_EXTRAS_LEM) \ + $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/$(ARCH)/riscv_types.lem \ generated_definitions/lem/$(ARCH)/riscv.lem @@ -317,7 +313,7 @@ riscv_rmem: generated_definitions/for-rmem/riscv_toFromInterp2.ml riscv_rmem: generated_definitions/for-rmem/riscv.defs .PHONY: riscv_rmem -generated_definitions/for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras +generated_definitions/for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras -lem_lib Mem_metadata generated_definitions/for-rmem/riscv.lem: $(SAIL_RMEM_SRCS) mkdir -p $(dir $@) # We do not need the isabelle .thy files, but sail always generates them diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem new file mode 100644 index 0000000..24bcecb --- /dev/null +++ b/handwritten_support/0.11/mem_metadata.lem @@ -0,0 +1,16 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +val write_ram : forall 'rv 'e 'n. Size 'n => write_kind -> mword ty64 -> integer -> mword 'n -> unit -> monad 'rv bool 'e +let write_ram wk addr width data meta = + write_mem wk () addr width data + +val read_ram : forall 'rv 'e 'n. Size 'n => read_kind -> mword ty64 -> integer -> bool -> monad 'rv (mword 'n * unit) 'e +let read_ram rk addr width read_tag = + read_mem rk () addr width >>= (fun (data : mword 'n) -> + return (data, ())) diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem new file mode 100644 index 0000000..24bcecb --- /dev/null +++ b/handwritten_support/mem_metadata.lem @@ -0,0 +1,16 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +val write_ram : forall 'rv 'e 'n. Size 'n => write_kind -> mword ty64 -> integer -> mword 'n -> unit -> monad 'rv bool 'e +let write_ram wk addr width data meta = + write_mem wk () addr width data + +val read_ram : forall 'rv 'e 'n. Size 'n => read_kind -> mword ty64 -> integer -> bool -> monad 'rv (mword 'n * unit) 'e +let read_ram rk addr width read_tag = + read_mem rk () addr width >>= (fun (data : mword 'n) -> + return (data, ())) diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index b8d47d0..6cc768c 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"} : 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"} : 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_fetch.sail b/model/riscv_fetch.sail index 64aff4b..d091756 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. diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index d02c49d..3fd6f31 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,49 @@ 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(paddr, width), default_meta) else if within_phys_mem(paddr, width) - then phys_mem_read(t, paddr, width, aq, rl, res) + then phys_mem_read(t, paddr, width, aq, rl, res, meta) else MemException(E_Load_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 +87,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 +101,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_sys_control.sail b/model/riscv_sys_control.sail index 8162cb8..3db3bbf 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -489,3 +489,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_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_sv39.sail b/model/riscv_vmem_sv39.sail index a1edc4e..6f9d7f0 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]), @@ -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..03d22c6 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]), @@ -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), |