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

Change ext_data_get_addr to use bytes for width

6 files changed, 30 insertions, 23 deletions

diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 345e78c..03ac69e 100644
--- 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
index f9c7835..0d29d4c 100644
--- 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
index 2e0eb9c..4264997 100644
--- 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
index 8d86804..c119ce9 100644
--- 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
index fcd4bb8..5c89e91 100644
--- 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
index ce9cd62..4da82e1 100644
--- 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)