Fix internal error caused by invalid LR / SC / AMO widths.

The RISC-V spec. only shows LR / SC / AMOs for word and double widths
even though the encoding would naturally extend to other widths (it is
a little unclear). Previously the Sail model would decode the unused
widths but throw an internal error in execute. With this change the
unused widths will not be decoded and will cause illegal instruction
exceptions instead.

1 files changed, 19 insertions, 6 deletions

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 55727b8..7b40985 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -20,11 +20,24 @@ function lrsc_width_str(width : word_width) -> string =
     DOUBLE => ".d"
   }
 
+/**
+ * RISC-V only appears to define LR / SC / AMOs for word and double, although
+ * there seem to be encodings reserved for other widths.
+ */
+function amo_width_valid(size : word_width) -> bool = {
+  match(size) {
+    WORD   => true,
+    DOUBLE => sizeof(xlen) >= 64,
+    _      => false
+  }
+} 
+
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 
-mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if word_width_bytes(size) <= sizeof(xlen_bytes)
-  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if word_width_bytes(size) <= sizeof(xlen_bytes)
+mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size)
+  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)
+
 
 /* We could set load-reservations on physical or virtual addresses.
  * For now we set them on virtual addresses, since it makes the
@@ -85,8 +98,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)
 
-mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if word_width_bytes(size) <= sizeof(xlen_bytes)
-  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if word_width_bytes(size) <= sizeof(xlen_bytes)
+mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid(size)
+  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
@@ -179,8 +192,8 @@ mapping encdec_amoop : amoop <-> bits(5) = {
   AMOMAXU <-> 0b11100
 }
 
-mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if word_width_bytes(size) <= sizeof(xlen_bytes)
-  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if word_width_bytes(size) <= sizeof(xlen_bytes)
+mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(size)
+  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */