From 717cb553b37863a27a114b81c008d9cb0e572b6e Mon Sep 17 00:00:00 2001 From: HAMZA-AFZAL404 Date: Tue, 23 Apr 2024 17:31:49 +0500 Subject: [PATCH] Renamed pmm with zpm --- c_emulator/riscv_platform.c | 4 ++-- c_emulator/riscv_platform.h | 2 +- c_emulator/riscv_platform_impl.c | 2 +- c_emulator/riscv_platform_impl.h | 2 +- c_emulator/riscv_sim.c | 4 ++-- handwritten_support/riscv_extras.lem | 6 +++--- handwritten_support/riscv_extras.v | 2 +- .../riscv_extras_sequential.lem | 6 +++--- model/riscv_insts_base.sail | 18 ++++++++++++------ model/riscv_sys_regs.sail | 10 +++++----- ocaml_emulator/platform.ml | 4 ++-- ocaml_emulator/riscv_ocaml_sim.ml | 6 +++--- 12 files changed, 36 insertions(+), 30 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 2d43f2484..12c8fe06f 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -47,9 +47,9 @@ bool sys_enable_writable_fiom(unit u) return rv_enable_writable_fiom; } -bool sys_enable_pmm(unit u) +bool sys_enable_zpm(unit u) { - return rv_enable_pmm; + return rv_enable_zpm; } bool sys_enable_vext(unit u) diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 242fe5ea4..a880d6e4a 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -8,7 +8,7 @@ bool sys_enable_zcb(unit); bool sys_enable_zfinx(unit); bool sys_enable_writable_misa(unit); bool sys_enable_writable_fiom(unit); -bool sys_enable_pmm(unit); +bool sys_enable_zpm(unit); bool sys_enable_vext(unit); uint64_t sys_pmp_count(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index a68835804..b37f28c4b 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -18,7 +18,7 @@ bool rv_enable_dirty_update = false; bool rv_enable_misaligned = false; bool rv_mtval_has_illegal_inst_bits = false; bool rv_enable_writable_fiom = true; -bool rv_enable_pmm = false; +bool rv_enable_zpm = false; uint64_t rv_ram_base = UINT64_C(0x80000000); uint64_t rv_ram_size = UINT64_C(0x4000000); diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index df4afdb68..461406b1b 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -22,7 +22,7 @@ extern bool rv_enable_dirty_update; extern bool rv_enable_misaligned; extern bool rv_mtval_has_illegal_inst_bits; extern bool rv_enable_writable_fiom; -extern bool rv_enable_pmm; +extern bool rv_enable_zpm; extern uint64_t rv_ram_base; extern uint64_t rv_ram_size; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 7ec8a5b4e..0874b4511 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -136,7 +136,7 @@ static struct option options[] = { {"report-arch", no_argument, 0, 'a' }, {"test-signature", required_argument, 0, 'T' }, {"signature-granularity", required_argument, 0, 'g' }, - {"enable-pmm", no_argument, 0, 'Y' }, + {"enable-zpm", no_argument, 0, 'Y' }, #ifdef RVFI_DII {"rvfi-dii", required_argument, 0, 'r' }, #endif @@ -318,7 +318,7 @@ static int process_args(int argc, char **argv) break; case 'Y': fprintf(stderr, "enabling pointer masking support.\n"); - rv_enable_pmm = true; + rv_enable_zpm = true; break; case 'I': fprintf(stderr, "disabling writable misa CSR.\n"); diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index fba6e0d95..a3eab79d7 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -169,9 +169,9 @@ val sys_enable_writable_fiom : unit -> bool let sys_enable_writable_fiom () = true declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom` -val sys_enable_pmm : unit -> bool -let sys_enable_pmm () = false -declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm` +val sys_enable_zpm : unit -> bool +let sys_enable_zpm () = false +declare ocaml target_rep function sys_enable_zpm = `Platform.enable_zpm` val plat_ram_base : unit -> bitvector let plat_ram_base () = [] diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index e680ab83d..aa870af01 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -201,7 +201,7 @@ Axiom sys_enable_fdext : unit -> bool. Axiom sys_enable_next : unit -> bool. Axiom sys_enable_zfinx : unit -> bool. Axiom sys_enable_writable_fiom : unit -> bool. -Axiom sys_enable_pmm : unit -> bool. +Axiom sys_enable_zpm : unit -> bool. (* The constraint solver can do this itself, but a Coq bug puts anonymous_subproof into the term instead of an actual subproof. *) diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 5dc8a17d7..0c6a9bc67 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -157,9 +157,9 @@ val sys_enable_writable_fiom : unit -> bool let sys_enable_writable_fiom () = true declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom` -val sys_enable_pmm : unit -> bool -let sys_enable_pmm () = false -declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm` +val sys_enable_zpm : unit -> bool +let sys_enable_zpm () = false +declare ocaml target_rep function sys_enable_zpm = `Platform.enable_zpm` val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 6eeee6506..5afc47d87 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -327,9 +327,9 @@ function transform_VA (effective_address : xlenbits,PMLEN :int) -> xlenbits = { let XLEN = sizeof(xlen); let i = XLEN -(PMLEN +1); let effective_bit = effective_address[i..i]; - let NVBITS = replicate_bits(effective_bit, PMLEN); - let VBITS = effective_address[i..0]; - NVBITS @ VBITS + let masked_bits = replicate_bits(effective_bit, PMLEN); + let unmasked_bits = effective_address[i..0]; + masked_bits @ unmasked_bits } function transform_PA (effective_address : xlenbits,PMLEN :int) -> xlenbits = { @@ -337,9 +337,9 @@ function transform_PA (effective_address : xlenbits,PMLEN :int) -> xlenbits = { assert(PMLEN <= 63, "PMLEN out of range"); let XLEN = sizeof(xlen); let i = XLEN -(PMLEN + 1); - let NVBITS = replicate_bits(0b0, PMLEN); - let VBITS = effective_address[i..0]; - NVBITS @ VBITS + let masked_bits = replicate_bits(0b0, PMLEN); + let unmasked_bits = effective_address[i..0]; + masked_bits @ unmasked_bits } function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = { @@ -353,6 +353,12 @@ function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = (0b11) => transform_PA (vaddr,16), } }, + (Sv39) => { + match (pmm_bits){ + (0b10) => transform_VA (vaddr,7), + (0b11) => transform_VA (vaddr,16), + } + }, (Sv48) => { match (pmm_bits){ (0b10) => transform_VA (vaddr,7), diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 0de09bb59..3fa93a91c 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -94,7 +94,7 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: " supervisor mode is implemented and non-bare addressing modes are supported. */ val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool /* whether the PME extension was enabled at boot */ -val sys_enable_pmm = {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : unit -> bool +val sys_enable_zpm = {c: "sys_enable_zpm", ocaml: "Platform.enable_zpm", _: "sys_enable_zpm"} : unit -> bool /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) @@ -841,7 +841,7 @@ register senvcfg : SEnvcfg function legalize_mseccfg(o : MSeccfg, v : xlenbits) -> MSeccfg = { let v = Mk_MSeccfg(v); // Update PMM field only if Pointer Masking is enabled and Written value is legal - let o = [o with PMM = if (sys_enable_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()]; + let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -850,7 +850,7 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { let v = Mk_MEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Update PMM field only if Pointer Masking is enabled and Written value is legal - let o = [o with PMM = if (sys_enable_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()]; + let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -859,7 +859,7 @@ function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { let v = Mk_SEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Update PMM field only if Pointer Masking is enabled and Written value is legal - let o = [o with PMM = if (sys_enable_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()]; + let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -907,7 +907,7 @@ function get_pmm() -> bits(2) = { match cur_privilege { Machine => mseccfg.PMM(), Supervisor => menvcfg.PMM(), - User => senvcfg.PMM(), + User => if haveSupMode() then senvcfg.PMM() else menvcfg.PMM(), } } diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 98bc5b0ea..54645e93e 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -15,7 +15,7 @@ let config_enable_writable_fiom = ref true let config_enable_vext = ref true let config_pmp_count = ref Big_int.zero let config_pmp_grain = ref Big_int.zero -let config_enable_pmm = ref false +let config_enable_zpm = ref false let set_config_pmp_count x = config_pmp_count := Big_int.of_int x let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x @@ -93,7 +93,7 @@ let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits let enable_zcb () = !config_enable_zcb let enable_zfinx () = false let enable_writable_fiom () = !config_enable_writable_fiom -let enable_pmm () = !config_enable_pmm +let enable_zpm () = !config_enable_zpm let pmp_count () = !config_pmp_count let pmp_grain () = !config_pmp_grain diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index db6ebce38..847688c0a 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -50,9 +50,9 @@ let options = Arg.align ([("-dump-dts", ("-enable-next", Arg.Set P.config_enable_next, " enable N extension"); - ("-enable-pmm", - Arg.Set P.config_enable_pmm, - " enable PMM support"); + ("-enable-zpm", + Arg.Set P.config_enable_zpm, + " enable zpm support"); ("-mtval-has-illegal-inst-bits", Arg.Set P.config_mtval_has_illegal_inst_bits, " mtval stores instruction bits on an illegal instruction exception");