Added pmm Support

c_emulator/riscv_platform.c

@@ -52,6 +52,11 @@ bool sys_enable_writable_fiom(unit u)
  return rv_enable_writable_fiom;
 }
 
+bool sys_enable_zpm(unit u)
+{
+ return rv_enable_zpm;
+}
+
 bool sys_enable_vext(unit u)
 {
  return rv_enable_vext;

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_zpm(unit);
 bool sys_enable_vext(unit);
 bool sys_enable_bext(unit);
 bool sys_enable_zicbom(unit);

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_zpm = false;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);

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_zpm;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;

c_emulator/riscv_sim.c

@@ -59,6 +59,7 @@ enum {
  OPT_ENABLE_ZICBOM,
  OPT_ENABLE_ZICBOZ,
  OPT_CACHE_BLOCK_SIZE,
+ OPT_ENABLE_ZPM,
 };
 
 static bool do_dump_dts = false;
@@ -145,6 +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_ZPM },
 #ifdef RVFI_DII
  {"rvfi-dii", required_argument, 0, 'r' },
 #endif
@@ -344,6 +346,10 @@ static int process_args(int argc, char **argv)
  fprintf(stderr, "enabling N extension.\n");
  rv_enable_next = true;
  break;
+ case OPT_ENABLE_ZPM:
+ fprintf(stderr, "enabling pointer masking support.\n");
+ rv_enable_zpm = true;
+ break;
  case 'I':
  fprintf(stderr, "disabling writable misa CSR.\n");
  rv_enable_writable_misa = false;

handwritten_support/riscv_extras.lem

@@ -169,6 +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`
 
+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`

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_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. *)

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_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
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

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"
@@ -162,6 +163,9 @@ 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"
+mapping clause csr_name_map = 0x757 <-> "mseccfgh"
 /* TODO: other hpm counters and events */
 /* trigger/debug */
 mapping clause csr_name_map = 0x7a0 <-> "tselect"

model/riscv_insts_aext.sail

@@ -72,6 +72,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
  */
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
+ let pmm = is_pmm_active();
  let width_bytes = size_bytes(width);
 
  // This is checked during decoding.
@@ -86,14 +87,15 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
  /* "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 },
+ 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 }
+ MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
  },
  }
  }
@@ -111,6 +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 width_bytes = size_bytes(width);
 
  // This is checked during decoding.
@@ -131,12 +134,13 @@ 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) => {
- if not(is_aligned(vaddr, width))
- then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); 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, Write(Data)) { /* Write and ReadWrite are equivalent here:
+ 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_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
  TR_Address(addr, _) => {
  // Check reservation with physical address.
  if not(match_reservation(addr)) then {
@@ -145,13 +149,13 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  } else {
  let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
  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(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 }
+ MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
  }
  }
  }
@@ -191,6 +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 'width_bytes = size_bytes(width);
 
  // This is checked during decoding.
@@ -202,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 {
@@ -230,7 +236,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
  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 }
+ MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
  }
  }
  }

model/riscv_insts_base.sail

@@ -320,7 +320,30 @@ 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 = {
+ sign_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0])
+}
+
+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 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
+ }
+}
+
 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);
 
@@ -332,15 +355,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 },
  },
  }
  },
@@ -377,6 +401,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 +413,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 }
  }
  }
  }

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,17 +382,19 @@ 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.
  Some extensions perform additional checks on address validity. */
  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"),
  };
  }