Replace sizeof(xlen_bytes) with xlen_bytes

model/riscv_insts_aext.sail

@@ -75,7 +75,7 @@ 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));
+  assert(width_bytes <= xlen_bytes);
 
   /* Get the address, X(rs1) (no offset).
     * Extensions might perform additional checks on address validity.
@@ -114,7 +114,7 @@ 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));
+  assert(width_bytes <= xlen_bytes);
 
   if speculate_conditional () == false then {
     /* should only happen in rmem
@@ -194,7 +194,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   let 'width_bytes = size_bytes(width);
 
   // This is checked during decoding.
-  assert(width_bytes <= sizeof(xlen_bytes));
+  assert(width_bytes <= xlen_bytes);
 
   /* Get the address, X(rs1) (no offset).
     * Some extensions perform additional checks on address validity.

model/riscv_insts_base.sail

@@ -302,8 +302,8 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo
 
 /* unsigned loads are only present for widths strictly less than xlen,
    signed loads also present for widths equal to xlen */
-mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
-  <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
+mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < xlen_bytes) | (not(is_unsigned) & size_bytes(size) <= xlen_bytes)
+  <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < xlen_bytes) | (not(is_unsigned) & size_bytes(size) <= xlen_bytes)
 
 val extend_value : forall 'n, 0 < 'n <= xlen. (bool, bits('n)) -> xlenbits
 function extend_value(is_unsigned, value) = if is_unsigned then zero_extend(value) else sign_extend(value)
@@ -325,7 +325,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   let width_bytes = size_bytes(width);
 
   // This is checked during decoding.
-  assert(width_bytes <= sizeof(xlen_bytes));
+  assert(width_bytes <= xlen_bytes);
 
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
@@ -371,8 +371,8 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
 /* ****************************************************************** */
 union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
 
-mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)              if size_bytes(size) <= sizeof(xlen_bytes)
-  <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes)
+mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)              if size_bytes(size) <= xlen_bytes
+  <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= xlen_bytes
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
@@ -381,7 +381,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
   let width_bytes = size_bytes(width);
 
   // This is checked during decoding.
-  assert(width_bytes <= sizeof(xlen_bytes));
+  assert(width_bytes <= xlen_bytes);
 
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */

model/riscv_insts_zbkb.sail

@@ -27,7 +27,7 @@ function clause execute (ZBKB_RTYPE(rs2, rs1, rd, op)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
   let result : xlenbits = match op {
-    RISCV_PACK  => rs2_val[(sizeof(xlen_bytes)*4 - 1)..0] @ rs1_val[(sizeof(xlen_bytes)*4 - 1)..0],
+    RISCV_PACK  => rs2_val[(xlen_bytes*4 - 1)..0] @ rs1_val[(xlen_bytes*4 - 1)..0],
     RISCV_PACKH => zero_extend(rs2_val[7..0] @ rs1_val[7..0])
   };
   X(rd) = result;
@@ -65,9 +65,9 @@ function clause execute (RISCV_ZIP(rs1, rd)) = {
   assert(xlen == 32);
   let rs1_val = X(rs1);
   var result : xlenbits = zeros();
-  foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
+  foreach (i from 0 to (xlen_bytes*4 - 1)) {
     result[i*2] = rs1_val[i];
-    result[i*2 + 1] = rs1_val[i + sizeof(xlen_bytes)*4];
+    result[i*2 + 1] = rs1_val[i + xlen_bytes*4];
   };
   X(rd) = result;
   RETIRE_SUCCESS
@@ -86,9 +86,9 @@ function clause execute (RISCV_UNZIP(rs1, rd)) = {
   assert(xlen == 32);
   let rs1_val = X(rs1);
   var result : xlenbits = zeros();
-  foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
+  foreach (i from 0 to (xlen_bytes*4 - 1)) {
     result[i] = rs1_val[i*2];
-    result[i + sizeof(xlen_bytes)*4] = rs1_val[i*2 + 1];
+    result[i + xlen_bytes*4] = rs1_val[i*2 + 1];
   };
   X(rd) = result;
   RETIRE_SUCCESS