Add xlen guards on double-word operations to make them RV64-only.

3 files changed, 43 insertions, 42 deletions

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 2f93cc5..922d729 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -32,7 +32,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
  * call to load_reservation in LR and cancel_reservation in SC.
  */
 
-val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
+val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
 function process_loadres(rd, addr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
     MemValue(result) => { load_reservation(addr); X(rd) = result; true },
@@ -53,17 +53,17 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
          DOUBLE => vaddr[2..0] == 0b000
        };
     /* "LR faults like a normal load, even though it's in the AMO major opcode space."
-       - Andrew Waterman, isa-dev, 10 Jul 2018.
+     * - Andrew Waterman, isa-dev, 10 Jul 2018.
      */
     if (~ (aligned))
     then { handle_mem_exception(vaddr, E_Load_Addr_Align); false }
     else match translateAddr(vaddr, Read, Data) {
            TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
            TR_Address(addr) =>
-             match width {
-               WORD   => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
-               DOUBLE => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
-               _      => internal_error("LOADRES expected WORD or DOUBLE")
+             match (width, xlen) {
+               (WORD, _)    => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
+               (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
+               _            => internal_error("LOADRES expected WORD or DOUBLE")
              }
          }
   } else {
@@ -114,19 +114,19 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
           match translateAddr(vaddr, Write, Data) {
             TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
             TR_Address(addr) => {
-              let eares : MemoryOpResult(unit) = match width {
-                WORD   => mem_write_ea(addr, 4, aq, rl, true),
-                DOUBLE => mem_write_ea(addr, 8, aq, rl, true),
-                _      => internal_error("STORECON expected word or double")
+              let eares : MemoryOpResult(unit) = match (width, xlen) {
+                (WORD, _)    => mem_write_ea(addr, 4, aq, rl, true),
+                (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true),
+                _            => internal_error("STORECON expected word or double")
               };
               match (eares) {
                 MemException(e) => { handle_mem_exception(addr, e); false },
                 MemValue(_) => {
                   rs2_val = X(rs2);
-                  let res : MemoryOpResult(bool) = match width {
-                    WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
-                    DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
-                    _      => internal_error("STORECON expected word or double")
+                  let res : MemoryOpResult(bool) = match (width, xlen) {
+                    (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
+                    (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
+                    _            => internal_error("STORECON expected word or double")
                   };
                   match (res) {
                     MemValue(true)  => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
@@ -175,19 +175,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     match translateAddr(vaddr, ReadWrite, Data) {
       TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) => {
-        let eares : MemoryOpResult(unit) = match width {
-          WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
-          DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true),
-          _      => internal_error ("AMO expected WORD or DOUBLE")
+        let eares : MemoryOpResult(unit) = match (width, xlen) {
+          (WORD, _)    => mem_write_ea(addr, 4, aq & rl, rl, true),
+          (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
+          _            => internal_error ("AMO expected WORD or DOUBLE")
         };
         rs2_val : xlenbits = X(rs2);
         match (eares) {
           MemException(e) => { handle_mem_exception(addr, e); false },
           MemValue(_) => {
-            let rval : MemoryOpResult(xlenbits) = match width {
-              WORD   => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
-              DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
-              _      => internal_error ("AMO expected WORD or DOUBLE")
+            let rval : MemoryOpResult(xlenbits) = match (width, xlen) {
+              (WORD, _)    => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
+              (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
+              _            => internal_error ("AMO expected WORD or DOUBLE")
             };
             match (rval) {
               MemException(e)  => { handle_mem_exception(addr, e); false },
@@ -207,10 +207,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                     AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
                   };
 
-                let wval : MemoryOpResult(bool) = match width {
-                  WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
-                  DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true),
-                  _      => internal_error("AMO expected WORD or DOUBLE")
+                let wval : MemoryOpResult(bool) = match (width, xlen) {
+                  (WORD, _)    => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
+                  (DOUBLE, 64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
+                  _            => internal_error("AMO expected WORD or DOUBLE")
                 };
                 match (wval) {
                   MemValue(true)  => { X(rd) = loaded; true },
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 7730ea7..f570fb2 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -265,13 +265,13 @@ union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, b
 mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if size_bits(size) != 0b11 | not_bool(is_unsigned)
   <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if size_bits(size) != 0b11 | not_bool(is_unsigned)
 
-val extend_value : forall 'n, 0 < 'n <= 8. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
+val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
 function extend_value(is_unsigned, value) = match (value) {
   MemValue(v)     => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits),
   MemException(e) => MemException(e)
 }
 
-val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
+val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
 function process_load(rd, addr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
     MemValue(result) => { X(rd) = result; true },
@@ -294,14 +294,14 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   else match translateAddr(vaddr, Read, Data) {
     TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
     TR_Address(addr) =>
-      match width {
-        BYTE   =>
+      match (width, xlen) {
+        (BYTE, _)   =>
 	  process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
-        HALF   =>
+        (HALF, _)   =>
 	  process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned),
-        WORD   =>
+        (WORD, _)   =>
 	  process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned),
-        DOUBLE =>
+        (DOUBLE, 64) =>
 	  process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned)
       }
   }
@@ -354,11 +354,11 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
         MemException(e) => { handle_mem_exception(addr, e); false },
         MemValue(_) => {
           let rs2_val = X(rs2);
-          let res : MemoryOpResult(bool) = match width {
-            BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
-            HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
-            WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
-            DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+          let res : MemoryOpResult(bool) = match (width, xlen) {
+            (BYTE, _)    => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
+            (HALF, _)    => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
+            (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
+            (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
           };
           match (res) {
             MemValue(true)     => true,
diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail
index d4b1b53..9130ec4 100644
--- a/model/riscv_xlen.sail
+++ b/model/riscv_xlen.sail
@@ -1,9 +1,10 @@
 /* Define the XLEN value for the architecture. */
 
 // type-level definitions
-type xlen : Int = 64
-type xlenbits   = bits(xlen)
+type xlen       : Int = 64
+type xlen_bytes : Int = 8
+type xlenbits         = bits(xlen)
 
 // value-level definitions
-let xlen : int(xlen) = 64
-let xlen_bytes       = 8    // byte-width of xlen bits
+let xlen : int(xlen)  = 64
+let xlen_bytes        = 8    // byte-width of xlen bits