Merge pull request #468 from Timmmm/user/timh/cheri_width_bytes

Change ext_data_get_addr to use bytes for width
riscv · Jun 3, 2024 · b15c0d3 · b15c0d3
2 parents e1663e9 + 9194dd5
commit b15c0d3
Show file tree

Hide file tree

Showing 6 changed files with 30 additions and 23 deletions.
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
@@ -80,8 +80,15 @@ instantiation sail_mem_write with
  because it means width argument can be fast native integer. It
  would be even better if it could be <= 8 bytes so that data can
  also be a 64-bit int but CHERI needs 128-bit accesses for
- capabilities and SIMD / vector instructions will also need more. */
-type max_mem_access : Int = 16
+ capabilities and SIMD / vector instructions will also need more.
+
+ The specific value does not matter (if it is >8) since anything up
+ to 2^64-1 will result in a native int being used for the width type.
+
+ 4096 was chosen because it is a page size, and a reasonable maximum
+ for cbo.zero.
+ */
+type max_mem_access : Int = 4096
 
 val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool
 

diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
@@ -54,7 +54,7 @@ type ext_data_addr_error = unit
 
 /* Default data addr is just base register + immediate offset (may be zero).
  Extensions might override and add additional checks. */
-function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(1, max_mem_access))
  -> Ext_DataAddr_Check(ext_data_addr_error) =
  let addr = X(base) + offset in
  Ext_DataAddr_OK(addr)

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
@@ -64,7 +64,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
  /* Get the address, X(rs1) (no offset).
  * Extensions might perform additional checks on address validity.
  */
- match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
+ match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) {
  Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
  Ext_DataAddr_OK(vaddr) => {
  let aligned : bool =
@@ -120,7 +120,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  /* Get the address, X(rs1) (no offset).
  * Extensions might perform additional checks on address validity.
  */
- match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
+ match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) {
  Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
  Ext_DataAddr_OK(vaddr) => {
  let aligned : bool =
@@ -205,7 +205,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
  /* Get the address, X(rs1) (no offset).
  * Some extensions perform additional checks on address validity.
  */
- match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) {
+ match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), size_bytes(width)) {
  Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
  Ext_DataAddr_OK(vaddr) => {
  match translateAddr(vaddr, ReadWrite(Data, Data)) {

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
@@ -326,7 +326,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
  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), width) {
+ 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)
@@ -382,7 +382,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
  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, Write(Data), 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)

diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
@@ -315,7 +315,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
  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), width) {
+ 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)
@@ -381,7 +381,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
  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), 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)

diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
@@ -81,7 +81,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) =
  vstart = to_bits(16, i);
  foreach (j from 0 to (nf - 1)) {
  let elem_offset = (i * nf + j) * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
+ 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)
@@ -149,7 +149,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  if vm_val[i] then { /* active segments */
  foreach (j from 0 to (nf - 1)) {
  let elem_offset = (i * nf + j) * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
+ match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
  Ext_DataAddr_Error(e) => {
  if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL }
  else {
@@ -251,7 +251,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem)
  vstart = to_bits(16, i);
  foreach (j from 0 to (nf - 1)) {
  let elem_offset = (i * nf + j) * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
+ 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)
@@ -322,7 +322,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e
  vstart = to_bits(16, i);
  foreach (j from 0 to (nf - 1)) {
  let elem_offset = i * rs2_val + j * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
+ 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)
@@ -388,7 +388,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_
  vstart = to_bits(16, i);
  foreach (j from 0 to (nf - 1)) {
  let elem_offset = i * rs2_val + j * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
+ 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)
@@ -460,7 +460,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index
  vstart = to_bits(16, i);
  foreach (j from 0 to (nf - 1)) {
  let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
+ 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)
@@ -551,7 +551,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
  vstart = to_bits(16, i);
  foreach (j from 0 to (nf - 1)) {
  let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
+ 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)
@@ -644,7 +644,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
  foreach (i from elem_to_align to (elem_per_reg - 1)) {
  vstart = to_bits(16, cur_elem);
  let elem_offset = cur_elem * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
+ 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)
@@ -668,7 +668,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
  foreach (i from 0 to (elem_per_reg - 1)) {
  vstart = to_bits(16, cur_elem);
  let elem_offset = cur_elem * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
+ 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)
@@ -726,7 +726,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
  foreach (i from elem_to_align to (elem_per_reg - 1)) {
  vstart = to_bits(16, cur_elem);
  let elem_offset : int = cur_elem * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
+ 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)
@@ -760,7 +760,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
  foreach (i from 0 to (elem_per_reg - 1)) {
  vstart = to_bits(16, cur_elem);
  let elem_offset = cur_elem * load_width_bytes;
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
+ 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)
@@ -828,7 +828,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
  if i < evl then { /* active elements */
  vstart = to_bits(16, i);
  if op == VLM then { /* load */
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), width_type) {
+ 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)
@@ -844,7 +844,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
  }
  }
  } else if op == VSM then { /* store */
- match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), width_type) {
+ 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)