From c22c5c2adc4ee252395e6940a0f5ed409c9c8838 Mon Sep 17 00:00:00 2001 From: HAMZA-AFZAL404 Date: Thu, 18 Apr 2024 15:04:29 +0500 Subject: [PATCH 1/5] Added pmm Support --- c_emulator/riscv_platform.c | 5 + c_emulator/riscv_platform.h | 1 + c_emulator/riscv_platform_impl.c | 1 + c_emulator/riscv_platform_impl.h | 1 + c_emulator/riscv_sim.c | 7 + handwritten_support/riscv_extras.lem | 3 + handwritten_support/riscv_extras.v | 1 + .../riscv_extras_sequential.lem | 4 + model/riscv_csr_map.sail | 2 + model/riscv_insts_aext.sail | 216 +++++++++++++----- model/riscv_insts_base.sail | 15 +- model/riscv_insts_fext.sail | 34 +-- model/riscv_insts_vext_mem.sail | 169 ++++++++------ model/riscv_insts_zicsr.sail | 9 + model/riscv_sys_control.sail | 5 + model/riscv_sys_regs.sail | 67 +++++- ocaml_emulator/platform.ml | 2 + ocaml_emulator/riscv_ocaml_sim.ml | 3 + 18 files changed, 386 insertions(+), 159 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index cbd3ae319..e8423cbf1 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -52,6 +52,11 @@ bool sys_enable_writable_fiom(unit u) return rv_enable_writable_fiom; } +bool sys_enable_pmm(unit u) +{ + return rv_enable_pmm; +} + bool sys_enable_vext(unit u) { return rv_enable_vext; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 58792319c..5d4e9bd0c 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -9,6 +9,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_vext(unit); bool sys_enable_bext(unit); bool sys_enable_zicbom(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index a76e683d4..e7e830dfe 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -22,6 +22,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; 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 d8acd3b59..fcc281df7 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -26,6 +26,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 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 3f812c5ec..016b91f79 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -145,6 +145,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' }, #ifdef RVFI_DII {"rvfi-dii", required_argument, 0, 'r' }, #endif @@ -156,6 +157,7 @@ static struct option options[] = { {"enable-zfinx", no_argument, 0, 'x' }, {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, {"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL }, + {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, {"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB }, {"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM }, {"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ }, @@ -289,6 +291,7 @@ static int process_args(int argc, char **argv) "T:" "g:" "h" + "Y" #ifdef RVFI_DII "r:" #endif @@ -344,6 +347,10 @@ static int process_args(int argc, char **argv) fprintf(stderr, "enabling N extension.\n"); rv_enable_next = true; break; + case 'Y': + fprintf(stderr, "enabling pointer masking support.\n"); + rv_enable_pmm = true; + break; case 'I': fprintf(stderr, "disabling writable misa CSR.\n"); rv_enable_writable_misa = false; diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 245a7fe80..895faafeb 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -176,6 +176,9 @@ declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` val sys_pmp_count : unit -> integer let sys_pmp_count () = 0 declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count` +val sys_enable_pmm : unit -> bool +let sys_enable_pmm () = false +declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm` 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 b17f75343..e680ab83d 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -201,6 +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. (* 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 5ffe482cd..a213f6833 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -157,6 +157,10 @@ 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 plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 6478919ca..78e223000 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -162,6 +162,8 @@ mapping clause csr_name_map = 0xB00 <-> "mcycle" mapping clause csr_name_map = 0xB02 <-> "minstret" mapping clause csr_name_map = 0xB80 <-> "mcycleh" mapping clause csr_name_map = 0xB82 <-> "minstreth" +/* machine security */ +mapping clause csr_name_map = 0x747 <-> "mseccfg" /* TODO: other hpm counters and events */ /* trigger/debug */ mapping clause csr_name_map = 0x7a0 <-> "tselect" diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 18c047e49..00cbe2dc8 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -72,29 +72,41 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) */ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { - let width_bytes = size_bytes(width); - - // This is checked during decoding. - assert(width_bytes <= sizeof(xlen_bytes)); - - /* Get the address, X(rs1) (no offset). - * Extensions might perform additional checks on address validity. - */ - match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => { - /* "LR faults like a normal load, even though it's in the AMO major opcode space." - * - Andrew Waterman, isa-dev, 10 Jul 2018. - */ - if not(is_aligned(vaddr, width)) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => - match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) { - MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - }, + let pmm = is_pmm_active(); + if haveAtomics() then { + /* Get the address, X(rs1) (no offset). + * Extensions might perform additional checks on address validity. + */ + 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 vaddr_ = transform_effective_address(vaddr, pmm); + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + */ + match width { + BYTE => true, + HALF => vaddr_[0..0] == 0b0, + WORD => vaddr_[1..0] == 0b00, + DOUBLE => vaddr_[2..0] == 0b000 + }; + /* "LR faults like a normal load, even though it's in the AMO major opcode space." + * - Andrew Waterman, isa-dev, 10 Jul 2018. + */ + if not(aligned) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL } + 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_loadres(rd, vaddr_, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false), + (HALF, _) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), + (WORD, _) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false), + (DOUBLE, 64) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + } + } } } } @@ -111,47 +123,68 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - let width_bytes = size_bytes(width); - - // This is checked during decoding. - assert(width_bytes <= sizeof(xlen_bytes)); - + let pmm = is_pmm_active(); if speculate_conditional () == false then { /* should only happen in rmem * rmem: allow SC to fail very early */ X(rd) = zero_extend(0b1); RETIRE_SUCCESS } else { - /* normal non-rmem case - * rmem: SC is allowed to succeed (but might fail later) - */ - /* Get the address, X(rs1) (no offset). - * Extensions might perform additional checks on address validity. - */ - match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => { - if not(is_aligned(vaddr, width)) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } - else { - 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, _) => { - // Check reservation with physical address. - if not(match_reservation(addr)) then { - /* cannot happen in rmem */ - X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS - } else { - let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); - match eares { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - MemValue(_) => { - let rs2_val = X(rs2); - match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) { - MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, - MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + if haveAtomics() then { + /* normal non-rmem case + * rmem: SC is allowed to succeed (but might fail later) + */ + /* Get the address, X(rs1) (no offset). + * Extensions might perform additional checks on address validity. + */ + 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 vaddr_ = transform_effective_address(vaddr, pmm); + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + */ + match width { + BYTE => true, + HALF => vaddr_[0..0] == 0b0, + WORD => vaddr_[1..0] == 0b00, + DOUBLE => vaddr_[2..0] == 0b000 + }; + if not(aligned) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } + else { + if match_reservation(vaddr_) == false then { + /* cannot happen in rmem */ + X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS + } else { + 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)) { + (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), + (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), + (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") + }; + match (eares) { + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true), + (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true), + (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") + }; + match (res) { + MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, + MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } + } } } } @@ -191,7 +224,56 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - let 'width_bytes = size_bytes(width); + let pmm = is_pmm_active(); + if haveAtomics() then { + /* Get the address, X(rs1) (no offset). + * Some extensions perform additional checks on address validity. + */ + match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let vaddr_ = transform_effective_address(vaddr, pmm) in + match translateAddr(vaddr_, ReadWrite(Data, Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), + (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), + (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + }; + let is_unsigned : bool = match op { + AMOMINU => true, + AMOMAXU => true, + _ => false + }; + let rs2_val : xlenbits = match width { + BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), + HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), + WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), + DOUBLE => X(rs2) + }; + match (eares) { + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, + MemValue(_) => { + let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)), + (HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)), + (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)), + (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + }; + match (mval) { + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, + MemValue(loaded) => { + let result : xlenbits = + match op { + AMOSWAP => rs2_val, + AMOADD => rs2_val + loaded, + AMOXOR => rs2_val ^ loaded, + AMOAND => rs2_val & loaded, + AMOOR => rs2_val | loaded, // This is checked during decoding. assert(width_bytes <= sizeof(xlen_bytes)); @@ -227,10 +309,18 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMINU => if rs2_val <_u loaded then rs2_val else loaded, AMOMAXU => if rs2_val >_u loaded then rs2_val else loaded, }; - match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) { - MemValue(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS }, - MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true), + (HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), + (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + }; + match (wval) { + MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, + MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } + } } } } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 438fa15d0..8b2df12d3 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -321,6 +321,7 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { + let pmm = is_pmm_active(); let offset : xlenbits = sign_extend(imm); let width_bytes = size_bytes(width); @@ -377,6 +378,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { + let pmm = is_pmm_active(); let offset : xlenbits = sign_extend(imm); let width_bytes = size_bytes(width); @@ -388,20 +390,21 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) { 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(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, TR_Address(paddr, _) => { let eares = mem_write_ea(paddr, width_bytes, aq, rl, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = X(rs2); match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) { MemValue(true) => RETIRE_SUCCESS, MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } } } } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 3a5509ea4..1291c16ec 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -315,26 +315,28 @@ function process_fload16(rd, addr, value) = } function clause execute(LOAD_FP(imm, rs1, rd, width)) = { + let pmm = is_pmm_active(); let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(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(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, TR_Address(addr, _) => { let (aq, rl, res) = (false, false, false); match (width) { BYTE => { handle_illegal(); RETIRE_FAIL }, HALF => - process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)), + process_fload16(rd, vaddr_, mem_read(Read(Data), addr, 2, aq, rl, res)), WORD => - process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), + process_fload32(rd, vaddr_, mem_read(Read(Data), addr, 4, aq, rl, res)), DOUBLE if sizeof(flen) >= 64 => - process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)), + process_fload64(rd, vaddr_, mem_read(Read(Data), addr, 8, aq, rl, res)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"), } } @@ -380,6 +382,7 @@ function process_fstore(vaddr, value) = } function clause execute (STORE_FP(imm, rs2, rs1, width)) = { + let pmm = is_pmm_active(); let offset : xlenbits = sign_extend(imm); let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. @@ -387,10 +390,11 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(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(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } + 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 { BYTE => MemValue () /* bogus placeholder for illegal size */, @@ -399,15 +403,15 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { DOUBLE => mem_write_ea(addr, 8, aq, rl, false) }; match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = F(rs2); match (width) { BYTE => { handle_illegal(); RETIRE_FAIL }, - HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), - WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), + HALF => process_fstore (vaddr_, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), + WORD => process_fstore (vaddr_, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), DOUBLE if sizeof(flen) >= 64 => - process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)), + process_fstore (vaddr_, mem_write_value(addr, 8, rs2_val, aq, rl, con)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"), }; } diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index b2fcc8c57..47cca08cf 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -69,6 +69,7 @@ mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ex val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -84,14 +85,15 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -135,6 +137,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled( val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -159,16 +162,17 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } }, Ext_DataAddr_OK(vaddr) => { - if check_misaligned(vaddr, width_type) then { - if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) then { + if i == 0 then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } else { vl = to_bits(sizeof(xlen), i); print_reg("CSR vl <- " ^ BitStr(vl)); trimmed = true } - } else match translateAddr(vaddr, Read(Data)) { + } else match translateAddr(vaddr_, Read(Data)) { TR_Failure(e, _) => { - if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + if i == 0 then { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } else { vl = to_bits(sizeof(xlen), i); print_reg("CSR vl <- " ^ BitStr(vl)); @@ -179,7 +183,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), MemException(e) => { - if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + if i == 0 then { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } else { vl = to_bits(sizeof(xlen), i); print_reg("CSR vl <- " ^ BitStr(vl)); @@ -240,6 +244,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -254,21 +259,22 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, MemValue(_) => { let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg)); let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); match (res) { MemValue(true) => (), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -309,6 +315,7 @@ mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnab val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -325,14 +332,15 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -376,6 +384,7 @@ mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEna val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -391,21 +400,22 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, MemValue(_) => { let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg)); let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); match (res) { MemValue(true) => (), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -446,7 +456,8 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { - let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); + let pmm = is_pmm_active(); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); @@ -463,14 +474,15 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { MemValue(elem) => write_single_element(EEW_data_bytes * 8, i, vd + to_bits(5, j * EMUL_data_reg), elem), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -538,7 +550,8 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { - let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); + let pmm = is_pmm_active(); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); @@ -554,21 +567,22 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, MemValue(_) => { let elem_val : bits('db * 8) = read_single_element(EEW_data_bytes * 8, i, vs3 + to_bits(5, j * EMUL_data_reg)); let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, elem_val, false, false, false); match (res) { MemValue(true) => (), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -633,6 +647,7 @@ mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if extensionEnabled(Ext_V) val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { + let pmm = is_pmm_active(); let width_type : word_width = size_bytes(load_width_bytes); let start_element = get_start_element(); if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ @@ -647,14 +662,15 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, cur_field), elem), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -671,14 +687,15 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j), elem), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -715,6 +732,7 @@ mapping clause encdec = VSRETYPE(nf, rs1, vs3) if extensionEnabled(Ext_V) val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { + let pmm = is_pmm_active(); let width_type : word_width = BYTE; let start_element = get_start_element(); if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ @@ -729,21 +747,22 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, MemValue(_) => { let elem : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, cur_field)); let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem, false, false, false); match (res) { MemValue(true) => (), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -763,20 +782,21 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, MemValue(_) => { let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); match (res) { MemValue(true) => (), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -820,6 +840,7 @@ mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V) val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { + let pmm = is_pmm_active(); let width_type : word_width = BYTE; let start_element = get_start_element(); let vd_or_vs3_val : vector('n, dec, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3); @@ -831,14 +852,15 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, 1, false, false, false) { MemValue(elem) => write_single_element(8, i, vd_or_vs3, elem), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } @@ -847,20 +869,21 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width_type) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr_, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }, MemValue(_) => { let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, vd_or_vs3_val[i], false, false, false); match (res) { MemValue(true) => (), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL } } } } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index f2980fb9e..349083587 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -56,6 +56,10 @@ function readCSR csr : csreg -> xlenbits = { (0x3D @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b10 @ idx)), (0x3E @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b11 @ idx)), + /* machine protection */ + (0x747, _) => mseccfg.bits()[sizeof(xlen) - 1 .. 0], + (0x757, 32) => mseccfg.bits()[63 .. 32], + /* machine mode counters */ (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], (0xB02, _) => minstret[(sizeof(xlen) - 1) .. 0], @@ -146,6 +150,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x3D @ idx : bits(4), _) => { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, (0x3E @ idx : bits(4), _) => { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, + /* machine protection */ + (0x747, 32) => { mseccfg = legalize_mseccfg(mseccfg, mseccfg.bits()[63 .. 32] @ value); Some(mseccfg.bits()[31 .. 0]) }, + (0x747, 64) => { mseccfg = legalize_mseccfg(mseccfg, value); Some(mseccfg.bits()) }, + (0x757, 32) => { mseccfg = legalize_mseccfg(mseccfg, value @ mseccfg.bits()[31 .. 0]); Some(mseccfg.bits()[63 .. 32]) }, + /* machine mode counters */ (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, (0xB02, _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; Some(value) }, diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index da04278b7..3f85a0a82 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -57,6 +57,10 @@ function is_CSR_defined (csr : csreg) -> bool = 0xB80 => sizeof(xlen) == 32, // mcycleh 0xB82 => sizeof(xlen) == 32, // minstreth + /* machine protection */ + 0x747 => p == Machine, // mseccfg + 0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh + /* disabled trigger/debug module */ 0x7a0 => true, @@ -541,6 +545,7 @@ function init_sys() -> unit = { minstret = zero_extend(0b0); minstret_increment = true; + mseccfg.bits = zero_extend(0b0); menvcfg.bits = zero_extend(0b0); senvcfg.bits = zero_extend(0b0); /* initialize vector csrs */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 295a4da19..c8115bf02 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -95,7 +95,8 @@ val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next", /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if supervisor mode is implemented and non-bare addressing modes are supported. */ val sys_enable_writable_fiom = pure {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 = pure {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : unit -> bool /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ val sys_pmp_count = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g. @@ -755,13 +756,40 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() +/* mseccfg is a XLEN-bit read/write register that controls */ +/* security features */ +bitfield MSeccfg : xlenbits = { + // Reserved WPRI bits. + wpri_2 : xlen - 1 .. 34, + // PMM bits of Pointer Masking Extension + PMM : 33 .. 32, + // Reserved WPRI bits. + wpri_1 : 31 .. 10, + // Supervisor SEED bits + SSEED : 9, + // User SEED bits + USEED : 8, + // Reserved WPRI bits. + wpri_0 : 7 .. 3, + // RLB bits + RLB : 2, + // Reserved WPRI bits. + MMWP : 1, + // MML bits + MML : 0, +} + bitfield MEnvcfg : bits(64) = { // Supervisor TimeCmp Extension STCE : 63, // Page Based Memory Types Extension PBMTE : 62, // Reserved WPRI bits. - wpri_1 : 61 .. 8, + wpri_2 : 61 .. 34, + // PMM bits of Pointer Masking Extension + PMM : 33 .. 32, + // Reserved WPRI bits. + wpri_1 : 31 .. 8, // Cache Block Zero instruction Enable CBZE : 7, // Cache Block Clean and Flush instruction Enable @@ -775,6 +803,8 @@ bitfield MEnvcfg : bits(64) = { } bitfield SEnvcfg : xlenbits = { + // PMM bits of Pointer Masking Extension + PMM : 33 .. 32, // Cache Block Zero instruction Enable CBZE : 7, // Cache Block Clean and Flush instruction Enable @@ -787,12 +817,23 @@ bitfield SEnvcfg : xlenbits = { FIOM : 0, } +register mseccfg : MSeccfg register menvcfg : MEnvcfg 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()]; + // Other extensions are not implemented yet so all other fields are read only zero. + o +} + 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()]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -800,6 +841,8 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { 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()]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -814,6 +857,17 @@ function is_fiom_active() -> bool = { User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1, } } + +// Return whether or not PMM is currently active, based on the current +// privilege and the menvcfg,senvcfg and mseccfg settings. +function is_pmm_active() -> bool = { + match cur_privilege { + Machine => (mseccfg.PMM() == 0b11 | mseccfg.PMM() == 0b10), + Supervisor => (menvcfg.PMM() == 0b11 | menvcfg.PMM() == 0b10), + User => ((menvcfg.PMM() == 0b11 | menvcfg.PMM() == 0b10) | (senvcfg.PMM() == 0b11 | senvcfg.PMM() == 0b10)), + } +} + /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vxsat : bits(1) @@ -831,6 +885,15 @@ bitfield Vtype : xlenbits = { } register vtype : Vtype +//Returns the PMM bits value depends on the Privilege mode +function get_pmm() -> bits(2) = { + match cur_privilege { + Machine => mseccfg.PMM(), + Supervisor => menvcfg.PMM(), + User => senvcfg.PMM(), + } +} + /* the dynamic selected element width (SEW) */ /* this returns the power of 2 for SEW */ val get_sew_pow : unit -> {3, 4, 5, 6} diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index b9921a0c3..dab5bc372 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -19,6 +19,7 @@ let config_enable_zicbom = ref false let config_enable_zicboz = ref false let config_pmp_count = ref Big_int.zero let config_pmp_grain = ref Big_int.zero +let config_enable_pmm = 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 @@ -106,6 +107,7 @@ let enable_svinval () = !config_enable_svinval 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 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 20eaef66f..96b76831e 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -50,6 +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"); ("-mtval-has-illegal-inst-bits", Arg.Set P.config_mtval_has_illegal_inst_bits, " mtval stores instruction bits on an illegal instruction exception"); From a64d196fe6445b49b4b6763d6f50c5b0f0d1a32e Mon Sep 17 00:00:00 2001 From: HAMZA-AFZAL404 Date: Tue, 23 Apr 2024 17:31:49 +0500 Subject: [PATCH 2/5] 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 | 66 +++++++++++++++++++ model/riscv_sys_regs.sail | 8 +-- ocaml_emulator/platform.ml | 4 +- ocaml_emulator/riscv_ocaml_sim.ml | 6 +- 12 files changed, 92 insertions(+), 20 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index e8423cbf1..ca38b8c70 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -52,9 +52,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 5d4e9bd0c..859cf97b2 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -9,7 +9,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); bool sys_enable_bext(unit); bool sys_enable_zicbom(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index e7e830dfe..7b6804894 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -22,7 +22,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 fcc281df7..67eb1ca38 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -26,7 +26,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 016b91f79..a4a57b9bd 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -145,7 +145,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 @@ -349,7 +349,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 895faafeb..2c45e9812 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -169,6 +169,7 @@ 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` +<<<<<<< HEAD val sys_pmp_grain : unit -> integer let sys_pmp_grain () = 0 declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` @@ -179,6 +180,11 @@ declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count` 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` +>>>>>>> 717cb55 (Renamed pmm with 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 a213f6833..c716641c5 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 8b2df12d3..79b9b64b5 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -318,7 +318,73 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool = // Return true if the address is misaligned and we don't support misaligned access. function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = +<<<<<<< HEAD not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) +======= + if plat_enable_misaligned_access() then false + else match width { + BYTE => false, + HALF => vaddr[0] == bitone, + WORD => vaddr[0] == bitone | vaddr[1] == bitone, + DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone + } +function transform_VA (effective_address : xlenbits,PMLEN :int) -> xlenbits = { + assert(PMLEN >= 0, "PMLEN out of range"); + assert(PMLEN <= 63, "PMLEN out of range"); + let XLEN = sizeof(xlen); + let i = XLEN -(PMLEN +1); + let effective_bit = effective_address[i..i]; + 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 = { + assert(PMLEN >= 0, "PMLEN out of range"); + assert(PMLEN <= 63, "PMLEN out of range"); + let XLEN = sizeof(xlen); + let i = XLEN -(PMLEN + 1); + 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 = { + if pmm then { + let pmm_bits : bits(2) = get_pmm(); + let mode : SATPMode = translationMode(cur_privilege); + match (mode) { + (Sbare) => { + match (pmm_bits){ + (0b10) => transform_PA (vaddr,7), + (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), + (0b11) => transform_VA (vaddr,16), + } + }, + (Sv57) => { + match (pmm_bits){ + (0b10) => transform_VA (vaddr,7), + (0b11) => transform_VA (vaddr,16), + } + }, + } + } + else { + vaddr //PMM is not active + } +} +>>>>>>> 717cb55 (Renamed pmm with zpm) function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let pmm = is_pmm_active(); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index c8115bf02..058a628d5 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -824,7 +824,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 } @@ -833,7 +833,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 } @@ -842,7 +842,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 } @@ -890,7 +890,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 dab5bc372..b407441f7 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -19,7 +19,7 @@ let config_enable_zicbom = ref false let config_enable_zicboz = ref false 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 @@ -107,7 +107,7 @@ let enable_svinval () = !config_enable_svinval 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 96b76831e..f075d1724 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"); From 07bd33b64958b0e693368d12c51383b5bb681820 Mon Sep 17 00:00:00 2001 From: HAMZA-AFZAL404 Date: Sun, 28 Jul 2024 11:29:04 +0500 Subject: [PATCH 3/5] Resolved Some Conflicts For PMM --- c_emulator/riscv_sim.c | 11 +- handwritten_support/riscv_extras.lem | 15 +- model/riscv_csr_map.sail | 2 + model/riscv_insts_aext.sail | 234 +++++++++------------------ model/riscv_insts_base.sail | 44 ++--- model/riscv_sys_regs.sail | 28 ++-- 6 files changed, 117 insertions(+), 217 deletions(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index a4a57b9bd..86793f5b4 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -59,6 +59,7 @@ enum { OPT_ENABLE_ZICBOM, OPT_ENABLE_ZICBOZ, OPT_CACHE_BLOCK_SIZE, + OPT_ENABLE_ZJPM, }; static bool do_dump_dts = false; @@ -134,7 +135,7 @@ static struct option options[] = { {"pmp-count", required_argument, 0, OPT_PMP_COUNT }, {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN }, {"enable-next", no_argument, 0, 'N' }, - {"ram-size", required_argument, 0, 'z' }, + {"ram-size", required_argument, 0, 'z' }, {"disable-compressed", no_argument, 0, 'C' }, {"disable-writable-misa", no_argument, 0, 'I' }, {"disable-fdext", no_argument, 0, 'F' }, @@ -145,7 +146,7 @@ static struct option options[] = { {"report-arch", no_argument, 0, 'a' }, {"test-signature", required_argument, 0, 'T' }, {"signature-granularity", required_argument, 0, 'g' }, - {"enable-zpm", no_argument, 0, 'Y' }, + {"enable-zpm", no_argument, 0, OPT_ENABLE_ZJPM }, #ifdef RVFI_DII {"rvfi-dii", required_argument, 0, 'r' }, #endif @@ -157,7 +158,6 @@ static struct option options[] = { {"enable-zfinx", no_argument, 0, 'x' }, {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, {"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL }, - {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, {"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB }, {"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM }, {"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ }, @@ -290,8 +290,7 @@ static int process_args(int argc, char **argv) "t:" "T:" "g:" - "h" - "Y" + "h" #ifdef RVFI_DII "r:" #endif @@ -347,7 +346,7 @@ static int process_args(int argc, char **argv) fprintf(stderr, "enabling N extension.\n"); rv_enable_next = true; break; - case 'Y': + case OPT_ENABLE_ZJPM: fprintf(stderr, "enabling pointer masking support.\n"); rv_enable_zpm = true; break; diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 2c45e9812..115c7fc69 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -169,7 +169,10 @@ 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` -<<<<<<< HEAD +val sys_enable_zpm : unit -> bool +let sys_enable_zpm () = false +declare ocaml target_rep function sys_enable_zpm = `Platform.enable_zpm` + val sys_pmp_grain : unit -> integer let sys_pmp_grain () = 0 declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` @@ -177,14 +180,6 @@ declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` val sys_pmp_count : unit -> integer let sys_pmp_count () = 0 declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count` -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` ->>>>>>> 717cb55 (Renamed pmm with zpm) val plat_ram_base : unit -> bitvector let plat_ram_base () = [] @@ -264,4 +259,4 @@ val print_bits : string -> bitvector -> unit let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs))) val print_dbg : string -> unit -let print_dbg msg = () +let print_dbg msg = () \ No newline at end of file diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 78e223000..a273ebcda 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -70,6 +70,7 @@ mapping clause csr_name_map = 0x306 <-> "mcounteren" mapping clause csr_name_map = 0x320 <-> "mcountinhibit" /* machine envcfg */ mapping clause csr_name_map = 0x30A <-> "menvcfg" +mapping clause csr_name_map = 0x31A <-> "menvcfgh" /* machine trap handling */ mapping clause csr_name_map = 0x340 <-> "mscratch" mapping clause csr_name_map = 0x341 <-> "mepc" @@ -164,6 +165,7 @@ mapping clause csr_name_map = 0xB80 <-> "mcycleh" mapping clause csr_name_map = 0xB82 <-> "minstreth" /* machine security */ mapping clause csr_name_map = 0x747 <-> "mseccfg" +mapping clause csr_name_map = 0x757 <-> "mseccfgh" /* TODO: other hpm counters and events */ /* trigger/debug */ mapping clause csr_name_map = 0x7a0 <-> "tselect" diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 00cbe2dc8..813f00d88 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -73,40 +73,30 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { let pmm = is_pmm_active(); - if haveAtomics() then { - /* Get the address, X(rs1) (no offset). - * Extensions might perform additional checks on address validity. - */ - 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 vaddr_ = transform_effective_address(vaddr, pmm); - let aligned : bool = - /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt - * to treat them as valid here; otherwise we'd need to throw an internal_error. - */ - match width { - BYTE => true, - HALF => vaddr_[0..0] == 0b0, - WORD => vaddr_[1..0] == 0b00, - DOUBLE => vaddr_[2..0] == 0b000 - }; - /* "LR faults like a normal load, even though it's in the AMO major opcode space." - * - Andrew Waterman, isa-dev, 10 Jul 2018. - */ - if not(aligned) - then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL } - 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_loadres(rd, vaddr_, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false), - (HALF, _) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), - (WORD, _) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false), - (DOUBLE, 64) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - } - } + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + + /* Get the address, X(rs1) (no offset). + * Extensions might perform additional checks on address validity. + */ + match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + /* "LR faults like a normal load, even though it's in the AMO major opcode space." + * - Andrew Waterman, isa-dev, 10 Jul 2018. + */ + let vaddr_ = transform_effective_address(vaddr, pmm); + if not(is_aligned(vaddr_, width)) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, + TR_Address(addr, _) => + match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) { + MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } + }, } } } @@ -123,68 +113,49 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + if speculate_conditional () == false then { /* should only happen in rmem * rmem: allow SC to fail very early */ X(rd) = zero_extend(0b1); RETIRE_SUCCESS } else { - if haveAtomics() then { - /* normal non-rmem case - * rmem: SC is allowed to succeed (but might fail later) - */ - /* Get the address, X(rs1) (no offset). - * Extensions might perform additional checks on address validity. - */ - 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 vaddr_ = transform_effective_address(vaddr, pmm); - let aligned : bool = - /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt - * to treat them as valid here; otherwise we'd need to throw an internal_error. - */ - match width { - BYTE => true, - HALF => vaddr_[0..0] == 0b0, - WORD => vaddr_[1..0] == 0b00, - DOUBLE => vaddr_[2..0] == 0b000 - }; - if not(aligned) - then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } - else { - if match_reservation(vaddr_) == false then { - /* cannot happen in rmem */ - X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS - } else { - 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)) { - (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), - (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") - }; - match (eares) { - MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, - MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true), - (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true), - (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") - }; - match (res) { - MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, - MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } - } + /* normal non-rmem case + * rmem: SC is allowed to succeed (but might fail later) + */ + /* Get the address, X(rs1) (no offset). + * Extensions might perform additional checks on address validity. + */ + match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let vaddr_ = transform_effective_address(vaddr, pmm); + if not(is_aligned(vaddr_, width)) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } + else { + 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, _) => { + // Check reservation with physical address. + if not(match_reservation(addr)) then { + /* cannot happen in rmem */ + X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS + } else { + let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); + match eares { + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, + MemValue(_) => { + let rs2_val = X(rs2); + match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) { + MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, + MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } } } } @@ -224,56 +195,8 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - let pmm = is_pmm_active(); - if haveAtomics() then { - /* Get the address, X(rs1) (no offset). - * Some extensions perform additional checks on address validity. - */ - match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm) in - match translateAddr(vaddr_, ReadWrite(Data, Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, - TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), - (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - let is_unsigned : bool = match op { - AMOMINU => true, - AMOMAXU => true, - _ => false - }; - let rs2_val : xlenbits = match width { - BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), - HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), - WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), - DOUBLE => X(rs2) - }; - match (eares) { - MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, - MemValue(_) => { - let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { - (BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)), - (HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)), - (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)), - (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - match (mval) { - MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, - MemValue(loaded) => { - let result : xlenbits = - match op { - AMOSWAP => rs2_val, - AMOADD => rs2_val + loaded, - AMOXOR => rs2_val ^ loaded, - AMOAND => rs2_val & loaded, - AMOOR => rs2_val | loaded, + let pmm = is_pmm_active(); + let 'width_bytes = size_bytes(width); // This is checked during decoding. assert(width_bytes <= sizeof(xlen_bytes)); @@ -284,18 +207,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - if not(is_aligned(vaddr, width)) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, ReadWrite(Data, Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm); + if not(is_aligned(vaddr_, width)) + then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr_, ReadWrite(Data, Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, TR_Address(addr, _) => { let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0]; match eares { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, MemValue(_) => { match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, MemValue(loaded) => { let result : bits('width_bytes * 8) = match op { @@ -309,18 +233,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMINU => if rs2_val <_u loaded then rs2_val else loaded, AMOMAXU => if rs2_val >_u loaded then rs2_val else loaded, }; - let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true), - (HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), - (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - match (wval) { - MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, - MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, - MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } - } + match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) { + MemValue(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS }, + MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL } } } } @@ -345,4 +261,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(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" + <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" \ No newline at end of file diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 79b9b64b5..73ec50af7 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -318,41 +318,29 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool = // Return true if the address is misaligned and we don't support misaligned access. function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = -<<<<<<< HEAD not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) -======= - if plat_enable_misaligned_access() then false - else match width { - BYTE => false, - HALF => vaddr[0] == bitone, - WORD => vaddr[0] == bitone | vaddr[1] == bitone, - DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone - } -function transform_VA (effective_address : xlenbits,PMLEN :int) -> xlenbits = { - assert(PMLEN >= 0, "PMLEN out of range"); - assert(PMLEN <= 63, "PMLEN out of range"); + +function transform_VA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = { let XLEN = sizeof(xlen); - let i = XLEN -(PMLEN +1); + let i = XLEN -(pmlen +1); let effective_bit = effective_address[i..i]; - let masked_bits = replicate_bits(effective_bit, PMLEN); + 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 = { - assert(PMLEN >= 0, "PMLEN out of range"); - assert(PMLEN <= 63, "PMLEN out of range"); +function transform_PA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = { let XLEN = sizeof(xlen); - let i = XLEN -(PMLEN + 1); - let masked_bits = replicate_bits(0b0, PMLEN); + let i = XLEN -(pmlen +1); + 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 = { if pmm then { - let pmm_bits : bits(2) = get_pmm(); - let mode : SATPMode = translationMode(cur_privilege); + let pmm_bits = get_pmm(); + let mode = translationMode(cur_privilege); match (mode) { (Sbare) => { match (pmm_bits){ @@ -384,7 +372,6 @@ function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = vaddr //PMM is not active } } ->>>>>>> 717cb55 (Renamed pmm with zpm) function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let pmm = is_pmm_active(); @@ -399,15 +386,16 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) { 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(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + let vaddr_ = transform_effective_address(vaddr, pmm) in + if check_misaligned(vaddr_, width) + then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr_, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, TR_Address(paddr, _) => match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) { MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }, }, } }, @@ -802,4 +790,4 @@ function clause execute SFENCE_VMA(rs1, rs2) = { } mapping clause assembly = SFENCE_VMA(rs1, rs2) - <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) \ No newline at end of file diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 058a628d5..2b6b25818 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -758,9 +758,9 @@ function write_seed_csr () -> option(xlenbits) = None() /* mseccfg is a XLEN-bit read/write register that controls */ /* security features */ -bitfield MSeccfg : xlenbits = { +bitfield MSeccfg : bits(64) = { // Reserved WPRI bits. - wpri_2 : xlen - 1 .. 34, + wpri_2 : 63 .. 34, // PMM bits of Pointer Masking Extension PMM : 33 .. 32, // Reserved WPRI bits. @@ -802,7 +802,7 @@ bitfield MEnvcfg : bits(64) = { FIOM : 0, } -bitfield SEnvcfg : xlenbits = { +bitfield SEnvcfg : bits(64) = { // PMM bits of Pointer Masking Extension PMM : 33 .. 32, // Cache Block Zero instruction Enable @@ -821,10 +821,10 @@ register mseccfg : MSeccfg register menvcfg : MEnvcfg register senvcfg : SEnvcfg -function legalize_mseccfg(o : MSeccfg, v : xlenbits) -> MSeccfg = { +function legalize_mseccfg(o : MSeccfg, v : bits(64)) -> 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_zpm() & (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 } @@ -833,16 +833,16 @@ 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_zpm() & (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 } -function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { +function legalize_senvcfg(o : SEnvcfg, v : bits(64)) -> 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_zpm() & (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 } @@ -862,9 +862,9 @@ function is_fiom_active() -> bool = { // privilege and the menvcfg,senvcfg and mseccfg settings. function is_pmm_active() -> bool = { match cur_privilege { - Machine => (mseccfg.PMM() == 0b11 | mseccfg.PMM() == 0b10), - Supervisor => (menvcfg.PMM() == 0b11 | menvcfg.PMM() == 0b10), - User => ((menvcfg.PMM() == 0b11 | menvcfg.PMM() == 0b10) | (senvcfg.PMM() == 0b11 | senvcfg.PMM() == 0b10)), + Machine => (mseccfg[PMM] == 0b11 | mseccfg[PMM] == 0b10), + Supervisor => (menvcfg[PMM] == 0b11 | menvcfg[PMM] == 0b10), + User => ((menvcfg[PMM] == 0b11 | menvcfg[PMM] == 0b10) | (senvcfg[PMM] == 0b11 | senvcfg[PMM] == 0b10)), } } @@ -888,9 +888,9 @@ register vtype : Vtype //Returns the PMM bits value depends on the Privilege mode function get_pmm() -> bits(2) = { match cur_privilege { - Machine => mseccfg.PMM(), - Supervisor => menvcfg.PMM(), - User => if haveSupMode() then senvcfg.PMM() else menvcfg.PMM(), + Machine => mseccfg[PMM], + Supervisor => menvcfg[PMM], + User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM], } } From e36958bb370f32908d0d05b44302bafada7f2f97 Mon Sep 17 00:00:00 2001 From: HAMZA-AFZAL404 Date: Sun, 28 Jul 2024 11:33:00 +0500 Subject: [PATCH 4/5] Updated the Zjpm --- model/riscv_sys_control.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3f85a0a82..48c8a5fd3 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -58,8 +58,8 @@ function is_CSR_defined (csr : csreg) -> bool = 0xB82 => sizeof(xlen) == 32, // minstreth /* machine protection */ - 0x747 => p == Machine, // mseccfg - 0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh + 0x747 => true, // mseccfg + 0x757 => sizeof(xlen) == 32, // mseccfgh /* disabled trigger/debug module */ 0x7a0 => true, From 0245007a9d2ce9ee29b81ea30639b324dba3e035 Mon Sep 17 00:00:00 2001 From: HAMZA-AFZAL404 Date: Mon, 16 Sep 2024 16:40:18 +0500 Subject: [PATCH 5/5] addressed some comments --- c_emulator/riscv_sim.c | 12 +++--- handwritten_support/riscv_extras.lem | 2 +- model/riscv_insts_aext.sail | 10 ++--- model/riscv_insts_base.sail | 55 ++++++---------------------- model/riscv_insts_vext_mem.sail | 14 +++---- model/riscv_sys_regs.sail | 42 ++++++++++++--------- 6 files changed, 56 insertions(+), 79 deletions(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 86793f5b4..943f0fc4e 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -59,7 +59,7 @@ enum { OPT_ENABLE_ZICBOM, OPT_ENABLE_ZICBOZ, OPT_CACHE_BLOCK_SIZE, - OPT_ENABLE_ZJPM, + OPT_ENABLE_ZPM, }; static bool do_dump_dts = false; @@ -135,7 +135,7 @@ static struct option options[] = { {"pmp-count", required_argument, 0, OPT_PMP_COUNT }, {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN }, {"enable-next", no_argument, 0, 'N' }, - {"ram-size", required_argument, 0, 'z' }, + {"ram-size", required_argument, 0, 'z' }, {"disable-compressed", no_argument, 0, 'C' }, {"disable-writable-misa", no_argument, 0, 'I' }, {"disable-fdext", no_argument, 0, 'F' }, @@ -146,7 +146,7 @@ static struct option options[] = { {"report-arch", no_argument, 0, 'a' }, {"test-signature", required_argument, 0, 'T' }, {"signature-granularity", required_argument, 0, 'g' }, - {"enable-zpm", no_argument, 0, OPT_ENABLE_ZJPM }, + {"enable-zpm", no_argument, 0, OPT_ENABLE_ZPM }, #ifdef RVFI_DII {"rvfi-dii", required_argument, 0, 'r' }, #endif @@ -290,7 +290,7 @@ static int process_args(int argc, char **argv) "t:" "T:" "g:" - "h" + "h" #ifdef RVFI_DII "r:" #endif @@ -346,10 +346,10 @@ static int process_args(int argc, char **argv) fprintf(stderr, "enabling N extension.\n"); rv_enable_next = true; break; - case OPT_ENABLE_ZJPM: + case OPT_ENABLE_ZPM: fprintf(stderr, "enabling pointer masking support.\n"); rv_enable_zpm = true; - break; + break; case 'I': fprintf(stderr, "disabling writable misa CSR.\n"); rv_enable_writable_misa = false; diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 115c7fc69..cf89b753c 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -259,4 +259,4 @@ val print_bits : string -> bitvector -> unit let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs))) val print_dbg : string -> unit -let print_dbg msg = () \ No newline at end of file +let print_dbg msg = () diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 813f00d88..820c48b47 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -113,7 +113,7 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let width_bytes = size_bytes(width); // This is checked during decoding. @@ -134,7 +134,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm); + let vaddr_ = transform_effective_address(vaddr, pmm); if not(is_aligned(vaddr_, width)) then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } else { @@ -195,7 +195,7 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let 'width_bytes = size_bytes(width); // This is checked during decoding. @@ -207,7 +207,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm); + let vaddr_ = transform_effective_address(vaddr, pmm); if not(is_aligned(vaddr_, width)) then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr_, ReadWrite(Data, Data)) { @@ -261,4 +261,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(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" \ No newline at end of file + <-> 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 73ec50af7..72f57ca4c 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -320,57 +320,26 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool = function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) -function transform_VA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = { - let XLEN = sizeof(xlen); - let i = XLEN -(pmlen +1); - let effective_bit = effective_address[i..i]; - let masked_bits = replicate_bits(effective_bit, pmlen); - let unmasked_bits = effective_address[i..0]; - masked_bits @ unmasked_bits +function transform_VA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = { + sign_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0]) } -function transform_PA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = { - let XLEN = sizeof(xlen); - let i = XLEN -(pmlen +1); - let masked_bits = replicate_bits(0b0, pmlen); - let unmasked_bits = effective_address[i..0]; - masked_bits @ unmasked_bits +function transform_PA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = { + zero_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0]) } function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = { if pmm then { let pmm_bits = get_pmm(); let mode = translationMode(cur_privilege); - match (mode) { - (Sbare) => { - match (pmm_bits){ - (0b10) => transform_PA (vaddr,7), - (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), - (0b11) => transform_VA (vaddr,16), - } - }, - (Sv57) => { - match (pmm_bits){ - (0b10) => transform_VA (vaddr,7), - (0b11) => transform_VA (vaddr,16), - } - }, + match pmm_bits { + pmm_mode(Enabled7) => if mode == Sbare then transform_PA(vaddr, 7) else transform_VA(vaddr, 7), + pmm_mode(Enabled16) => if mode == Sbare then transform_PA(vaddr, 16) else transform_VA(vaddr, 16), } - } - else { - vaddr //PMM is not active - } + } + else { + vaddr + } } function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { @@ -790,4 +759,4 @@ function clause execute SFENCE_VMA(rs1, rs2) = { } mapping clause assembly = SFENCE_VMA(rs1, rs2) - <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) \ No newline at end of file + <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 47cca08cf..f71810c09 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -137,7 +137,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled( val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -162,7 +162,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } }, Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm) in + let vaddr_ = transform_effective_address(vaddr, pmm) in if check_misaligned(vaddr_, width_type) then { if i == 0 then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } else { @@ -244,7 +244,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -457,7 +457,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let pmm = is_pmm_active(); - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); @@ -551,7 +551,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let pmm = is_pmm_active(); - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); @@ -567,7 +567,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - let vaddr_ = transform_effective_address(vaddr, pmm) in + let vaddr_ = transform_effective_address(vaddr, pmm) in if check_misaligned(vaddr_, width_type) then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr_, Write(Data)) { @@ -840,7 +840,7 @@ mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V) val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let width_type : word_width = BYTE; let start_element = get_start_element(); let vd_or_vs3_val : vector('n, dec, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 2b6b25818..2f12c5cbd 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -96,7 +96,7 @@ val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next", supervisor mode is implemented and non-bare addressing modes are supported. */ val sys_enable_writable_fiom = pure {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 = pure {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : unit -> bool +val sys_enable_zpm = pure {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 = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g. @@ -756,6 +756,21 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() +/* Pointer Masking Different modes */ +enum PointerMaskingMode = { + Disabled, // Pointer Masking Disabled + Reserved, // Reserved Encoding for Pointer Masking + Enabled7, // Pointer Masking Enabled with PMM = 7 + Enabled16, // Pointer Masking Enabled with PMM = 16 +} + +mapping pmm_mode : PointerMaskingMode <-> bits(2) = { + Disabled <-> 0b00, + Reserved <-> 0b01, + Enabled7 <-> 0b10, + Enabled16 <-> 0b11, +} + /* mseccfg is a XLEN-bit read/write register that controls */ /* security features */ bitfield MSeccfg : bits(64) = { @@ -824,7 +839,7 @@ register senvcfg : SEnvcfg function legalize_mseccfg(o : MSeccfg, v : bits(64)) -> 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_zpm() & (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] != pmm_mode(Reserved))) then v[PMM] else o[PMM]]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -833,7 +848,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_zpm() & (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] != pmm_mode(Reserved))) then v[PMM] else o[PMM]]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -842,7 +857,7 @@ function legalize_senvcfg(o : SEnvcfg, v : bits(64)) -> 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_zpm() & (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] != pmm_mode(Reserved))) then v[PMM] else o[PMM]]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -858,16 +873,6 @@ function is_fiom_active() -> bool = { } } -// Return whether or not PMM is currently active, based on the current -// privilege and the menvcfg,senvcfg and mseccfg settings. -function is_pmm_active() -> bool = { - match cur_privilege { - Machine => (mseccfg[PMM] == 0b11 | mseccfg[PMM] == 0b10), - Supervisor => (menvcfg[PMM] == 0b11 | menvcfg[PMM] == 0b10), - User => ((menvcfg[PMM] == 0b11 | menvcfg[PMM] == 0b10) | (senvcfg[PMM] == 0b11 | senvcfg[PMM] == 0b10)), - } -} - /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vxsat : bits(1) @@ -886,13 +891,16 @@ bitfield Vtype : xlenbits = { register vtype : Vtype //Returns the PMM bits value depends on the Privilege mode -function get_pmm() -> bits(2) = { +function get_pmm() -> bits(2) = match cur_privilege { Machine => mseccfg[PMM], Supervisor => menvcfg[PMM], - User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM], + User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM], } -} + +// Return whether or not PMM is currently active, based on the current +// privilege and the menvcfg,senvcfg and mseccfg settings. +function is_pmm_active() -> bool = get_pmm() != zeros(2) /* the dynamic selected element width (SEW) */ /* this returns the power of 2 for SEW */