Merge branch 'master' into rsnikhil

11 files changed, 84 insertions, 61 deletions

diff --git a/Makefile b/Makefile
index 0bddcfd..dcd738e 100644
--- a/Makefile
+++ b/Makefile
@@ -60,10 +60,10 @@ SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
 SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS)
 
 SAIL_ARCH_SRCS = $(PRELUDE)
-SAIL_ARCH_SRCS += riscv_types_ext.sail riscv_types.sail
+SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail
 SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail
 SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
-SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS)
+SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS)
 
 SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
 RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail
diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v
index 0e53888..e70d395 100644
--- a/handwritten_support/mem_metadata.v
+++ b/handwritten_support/mem_metadata.v
@@ -6,6 +6,6 @@ Require Import Sail2_prompt.
 
 Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v.
 
-Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e :=
+Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size) * unit) e :=
   read_mem rk a addr size >>= fun data =>
   returnm (data, tt).
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v
index 84f6761..7e350ed 100644
--- a/handwritten_support/riscv_extras.v
+++ b/handwritten_support/riscv_extras.v
@@ -45,12 +45,12 @@ val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => inte
 val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
 *)
 
-Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize)                         `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size.
-Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)                 `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addrsize addr size.
-Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)          `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addrsize addr size.
-Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize)                `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addrsize addr size.
-Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)        `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addrsize addr size.
-Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_strong_acquire addrsize addr size.
+Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize)                         `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size.
+Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)                 `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addrsize addr size.
+Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)          `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addrsize addr size.
+Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize)                `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addrsize addr size.
+Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)        `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addrsize addr size.
+Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_strong_acquire addrsize addr size.
 
 (*
 val MEMw                            : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
@@ -87,14 +87,14 @@ Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%st
 Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
 Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
 (*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
-Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len).
+Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >=? 0)} : monad rv (vec a len) e := returnm (vec_init u len).
 (*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
-Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0).
+Definition undefined_bitvector {rv e} len `{ArithFact (len >=? 0)} : monad rv (mword len) e := returnm (mword_of_int 0).
 (*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
 Definition undefined_bits {rv e} := @undefined_bitvector rv e.
 Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU.
 (*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*)
-Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i).
+Definition undefined_range {rv e} i j `{ArithFact (i <=? j)} : monad rv {z : Z & ArithFact (i <=? z <=? j)} e := returnm (build_ex i).
 Definition undefined_atom {rv e} i : monad rv Z e := returnm i.
 Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
 
@@ -119,10 +119,12 @@ Definition eq_bit (x : bitU) (y : bitU) : bool :=
   end.
 
 Require Import Zeuclid.
-Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}.
+Definition euclid_modulo (m n : Z) `{ArithFact (n >? 0)} : {z : Z & ArithFact (0 <=? z <=? n-1)}.
 apply existT with (x := ZEuclid.modulo m n).
 constructor.
 destruct H.
+unbool_comparisons.
+unbool_comparisons_goal.
 assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. }
 rewrite <- H at 3.
 lapply (ZEuclid.mod_always_pos m n); omega.
diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail
index 8c0cc17..9220534 100644
--- a/model/riscv_csr_ext.sail
+++ b/model/riscv_csr_ext.sail
@@ -1,8 +1,12 @@
 
-/* numeric fallback XXX apparent sail bug prevents this from compiling for C  */
-//mapping clause csr_name_map = reg <-> "UNKNOWN CSR: " ^ hex_bits_12(reg)
+mapping clause csr_name_map = reg <-> hex_bits_12(reg)
 end csr_name_map
 
+/* XXX due to an apparent Sail bug the definition of this function must appear
+   after the last csr_name_map clause and not by the val spec as it was 
+   previously. */
+function csr_name(csr) = csr_name_map(csr)
+
 function clause ext_is_CSR_defined(_, _) = false
 end ext_is_CSR_defined
 
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 7ec161b..ba52da6 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -93,7 +93,6 @@ mapping clause csr_name_map = 0x7a2  <-> "tdata2"
 mapping clause csr_name_map = 0x7a3  <-> "tdata3"
 
 val csr_name : csreg -> string
-function csr_name(csr) = csr_name_map(csr)
 overload to_str = {csr_name}
 
 /* Extensions may want to add additional CSR registers to the CSR address map.
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index f430a75..e760b90 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -198,21 +198,30 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
             let eares : MemoryOpResult(unit) = match (width, sizeof(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")
+              _            => internal_error("AMO expected WORD or DOUBLE")
+            };
+            let is_unsigned : bool = match op {
+              AMOMINU => true,
+              AMOMAXU => true,
+              _       => false
+            };
+            let rs2_val : xlenbits = match width {
+              WORD   => if is_unsigned then EXTZ(X(rs2)[31..0]) else EXTS(X(rs2)[31..0]),
+              DOUBLE => X(rs2),
+              _      => internal_error("AMO expected WORD or DOUBLE")
             };
-            rs2_val : xlenbits = X(rs2);
             match (eares) {
               MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
               MemValue(_) => {
-                let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
-                  (WORD, _)    => extend_value(false, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
-                  (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)),
-                  _            => internal_error ("AMO expected WORD or DOUBLE")
+                let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
+                  (WORD, _)    => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
+                  (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)),
+                  _            => internal_error("AMO expected WORD or DOUBLE")
                 };
-                match (rval) {
+                match (mval) {
                   MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL },
                   MemValue(loaded) => {
-                    result  : xlenbits =
+                    let result : xlenbits =
                       match op {
                         AMOSWAP => rs2_val,
                         AMOADD  => rs2_val + loaded,
@@ -228,14 +237,18 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                         AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
                         AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
                       };
-
+                    let rval : xlenbits = match width {
+                      WORD   => EXTS(loaded[31..0]),
+                      DOUBLE => loaded,
+                      _      => internal_error("AMO expected WORD or DOUBLE")
+                    };
                     let wval : MemoryOpResult(bool) = match (width, sizeof(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; RETIRE_SUCCESS },
+                      MemValue(true)  => { X(rd) = rval; RETIRE_SUCCESS },
                       MemValue(false) => { internal_error("AMO got false from mem_write_value") },
                       MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
                     }
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 056f537..3a23d9a 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -208,6 +208,6 @@ mapping csr_mnemonic : csrop <-> string = {
 }
 
 mapping clause assembly = CSR(csr, rs1, rd, true, op)
-  <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ csr_name_map(csr)
+  <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ hex_bits_12(csr)
 mapping clause assembly = CSR(csr, rs1, rd, false, op)
-  <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ csr_name_map(csr)
+  <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(csr)
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 25065ab..b3fa37d 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -80,7 +80,8 @@ function rvfi_read (addr, width, result) = {
     MemValue(v) => if   width <= 8
                    then { rvfi_exec->rvfi_mem_rdata() = sail_zero_extend(v,64);
                           rvfi_exec->rvfi_mem_rmask() = rvfi_encode_width_mask(width) }
-                   else (),
+                   else { rvfi_exec->rvfi_mem_rdata() = v[63..0];
+                          rvfi_exec->rvfi_mem_rmask() = 0xFF},
     MemException(_) => ()
   };
 }
@@ -91,38 +92,28 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))             effect {wreg, rmem, rmemt, rreg, escape}
-val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {wreg, rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
 $else
-val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))             effect {rmem, rmemt, rreg, escape}
-val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
 $endif
 
-function mem_read (typ, paddr, width, aq, rl, res) = {
- let result : MemoryOpResult(bits(8 * 'n)) =
-  if (aq | res) & (~ (is_aligned_addr(paddr, width)))
-  then MemException(E_Load_Addr_Align())
-  else match (aq, rl, res) {
-    (false, true,  false) => throw(Error_not_implemented("load.rl")),
-    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (_, _, _)             => MemoryOpResult_drop_meta(pmp_mem_read(typ, paddr, width, aq, rl, res, false))
-  };
- rvfi_read(paddr, width, result);
- result
+function mem_read_meta (typ, paddr, width, aq, rl, res, meta) = {
+  let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
+    if (aq | res) & (~ (is_aligned_addr(paddr, width)))
+    then MemException(E_Load_Addr_Align())
+    else match (aq, rl, res) {
+      (false, true,  false) => throw(Error_not_implemented("load.rl")),
+      (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
+      (_, _, _)             => pmp_mem_read(typ, paddr, width, aq, rl, res, meta)
+    };
+  rvfi_read(paddr, width, MemoryOpResult_drop_meta(result));
+  result
 }
 
-function mem_read_meta (typ, addr, width, aq, rl, res) = {
- let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
-  if (aq | res) & (~ (is_aligned_addr(addr, width)))
-  then MemException(E_Load_Addr_Align())
-  else match (aq, rl, res) {
-    (false, true,  false) => throw(Error_not_implemented("load.rl")),
-    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (_, _, _)             => pmp_mem_read(typ, addr, width, aq, rl, res, true)
-  };
- rvfi_read(addr, width, MemoryOpResult_drop_meta(result));
- result
-}
+function mem_read (typ, paddr, width, aq, rl, res) =
+  MemoryOpResult_drop_meta(mem_read_meta(typ, paddr, width, aq, rl, res, false))
 
 val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
 
@@ -148,6 +139,9 @@ function rvfi_write (addr, width, value) = {
   if width <= 8 then {
     rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(value,64);
     rvfi_exec->rvfi_mem_wmask() = rvfi_encode_width_mask(width);
+  } else {
+    rvfi_exec->rvfi_mem_wdata() = value[63..0];
+    rvfi_exec->rvfi_mem_wmask() = 0xFF;
   }
 }
 $else
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index cacf0db..987743a 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -108,8 +108,6 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 /* architectural interrupt definitions */
 
-type exc_code = bits(8)
-
 enum InterruptType = {
   I_U_Software,
   I_S_Software,
@@ -181,7 +179,7 @@ function exceptionType_to_bits(e) =
     E_SAMO_Page_Fault()    => 0x0f,
 
     /* extensions */
-    E_Extension(e)         => 0x18    /* First code for a custom extension */
+    E_Extension(e)         => ext_exc_type_to_bits(e)
   }
 
 val num_of_ExceptionType : ExceptionType -> {'n, (0 <= 'n < xlen). int('n)}
@@ -205,7 +203,7 @@ function num_of_ExceptionType(e) =
     E_SAMO_Page_Fault()    => 15,
 
     /* extensions */
-    E_Extension(e)         => 24    /* First code for a custom extension */
+    E_Extension(e)         => num_of_ext_exc_type(e)
 
   }
 
@@ -230,7 +228,7 @@ function exceptionType_to_str(e) =
     E_SAMO_Page_Fault()    => "store/amo-page-fault",
 
     /* extensions */
-    E_Extension(e)         => "extension-exception"
+    E_Extension(e)         => ext_exc_type_to_str(e)
   }
 
 overload to_str = {exceptionType_to_str}
diff --git a/model/riscv_types_common.sail b/model/riscv_types_common.sail
new file mode 100644
index 0000000..9db34a0
--- /dev/null
+++ b/model/riscv_types_common.sail
@@ -0,0 +1 @@
+type exc_code = bits(8)
diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail
index 5a05c39..6562981 100644
--- a/model/riscv_types_ext.sail
+++ b/model/riscv_types_ext.sail
@@ -20,3 +20,15 @@ type ext_exc_type = unit /* No exception extensions */
 /* Default translation of PTW errors into exception annotations */
 function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
   e
+
+/* Default conversion of extension exceptions to bits */
+val ext_exc_type_to_bits : ext_exc_type -> exc_code
+function ext_exc_type_to_bits(e) = 0x18 /* First code for a custom extension */
+
+/* Default conversion of extension exceptions to integers */
+val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
+function num_of_ext_exc_type(e) = 24 /* First code for a custom extension */
+
+/* Default conversion of extension exceptions to strings */
+val ext_exc_type_to_str : ext_exc_type -> string
+function ext_exc_type_to_str(e) = "extension-exception"