Merge branch 'riscv:master' into master

rsnikhil · Mar 25, 2024 · 932469c · 932469c
2 parents 4bee248 + 51b9732
commit 932469c
Show file tree

Hide file tree

Showing 13 changed files with 89 additions and 71 deletions.
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
@@ -288,7 +288,7 @@ static int process_args(int argc, char **argv)
       break;
     case OPT_PMP_COUNT:
       pmp_count = atol(optarg);
-      fprintf(stderr, "PMP count: %lld\n", pmp_count);
+      fprintf(stderr, "PMP count: %" PRIu64 "\n", pmp_count);
       if (pmp_count != 0 && pmp_count != 16 && pmp_count != 64) {
         fprintf(stderr, "invalid PMP count: must be 0, 16 or 64");
         exit(1);
@@ -297,7 +297,7 @@ static int process_args(int argc, char **argv)
       break;
     case OPT_PMP_GRAIN:
       pmp_grain = atol(optarg);
-      fprintf(stderr, "PMP grain: %lld\n", pmp_grain);
+      fprintf(stderr, "PMP grain: %" PRIu64 "\n", pmp_grain);
       if (pmp_grain >= 64) {
         fprintf(stderr, "invalid PMP grain: must less than 64");
         exit(1);

diff --git a/model/prelude.sail b/model/prelude.sail
@@ -66,7 +66,7 @@ overload min = {min_int}
 
 overload max = {max_int}
 
-val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
 
 val print = "print_endline" : string -> unit
 val print_string = "print_string" : (string, string) -> unit
@@ -112,7 +112,7 @@ function bit_to_bool b = match b {
   bitzero => false
 }
 
-val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
+val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l)
 function to_bits (l, n) = get_slice_int(l, n, 0)
 
 infix 4 <_s
@@ -148,8 +148,8 @@ infix 7 <<
 val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
 val "shift_bits_left"  : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
 
-val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
-val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), int('n)) -> bits('m)
+val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), int('n)) -> bits('m)
 
 overload operator >> = {shift_bits_right, shiftr}
 overload operator << = {shift_bits_left, shiftl}
@@ -175,11 +175,11 @@ val rotate_bits_left : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n)
 function rotate_bits_left (v, n) =
     (v << n) | (v >> (to_bits(length(n), length(v)) - n))
 
-val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), int('n)) -> bits('m)
 function rotater (v, n) =
     (v >> n) | (v << (length(v) - n))
 
-val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), int('n)) -> bits('m)
 function rotatel (v, n) =
     (v << n) | (v >> (length(v) - n))
 

diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
@@ -27,7 +27,7 @@
    capabilities and SIMD / vector instructions will also need more. */
 type max_mem_access : Int = 16
 
-val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool
+val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool
 function write_ram(wk, addr, width, data, meta) = {
   /* Write out metadata only if the value write succeeds.
    * It is assumed for now that this write always succeeds;
@@ -41,14 +41,14 @@ function write_ram(wk, addr, width, data, meta) = {
   ret
 }
 
-val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit
+val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n)) -> unit
 function write_ram_ea(wk, addr, width) =
   __write_mem_ea(wk, sizeof(xlen), addr, width)
 
-val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta)
+val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta)
 function read_ram(rk, addr, width, read_meta) =
   let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
   (__read_mem(rk, sizeof(xlen), addr, width), meta)
 
-val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
-val __TraceMemoryRead  : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
+val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
+val __TraceMemoryRead  : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail
@@ -14,8 +14,8 @@ type mem_meta = unit
 
 let default_meta : mem_meta = ()
 
-val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit
+val __WriteRAM_Meta : forall 'n. (xlenbits, int('n), mem_meta) -> unit
 function __WriteRAM_Meta(addr, width, meta) = ()
 
-val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta
+val __ReadRAM_Meta  : forall 'n. (xlenbits, int('n)) -> mem_meta
 function __ReadRAM_Meta(addr, width) = ()
diff --git a/model/riscv_addr_checks_common.sail b/model/riscv_addr_checks_common.sail
@@ -40,12 +40,12 @@ union Ext_PhysAddr_Check = {
  * return Some(exception) to abort the read or None to allow it to proceed. The
  * check is performed after PMP checks and does not apply to MMIO memory.
  */
-val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check
+val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check
 
 /*!
  * Validate a write to physical memory.
  * THIS(write_kind, paddr, size, data, metadata) should return Some(exception)
  * to abort the write or None to allow it to proceed. The check is performed
  * after PMP checks and does not apply to MMIO memory.
  */
-val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check
+val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
@@ -224,9 +224,9 @@ mapping clause assembly = C_LUI(imm, rd)
 union clause ast = C_SRLI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_SRLI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
   <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
-      if nzui5 @ nzui40 != 0b000000
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
 
 function clause execute (C_SRLI(shamt, rsd)) = {
   let rsd = creg2reg_idx(rsd);
@@ -242,9 +242,9 @@ mapping clause assembly = C_SRLI(shamt, rsd)
 union clause ast = C_SRAI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_SRAI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
   <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
-      if nzui5 @ nzui40 != 0b000000
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
 
 function clause execute (C_SRAI(shamt, rsd)) = {
   let rsd = creg2reg_idx(rsd);

diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
@@ -122,10 +122,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x304,  _) => { mie = legalize_mie(mie, value); Some(mie.bits) },
     (0x305,  _) => { Some(set_mtvec(value)) },
     (0x306,  _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) },
-    (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) },
-    (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits) },
+    (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) },
+    (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits) },
     (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now
-    (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) },
+    (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) },
     (0x320,  _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) },
     (0x340,  _) => { mscratch = value; Some(mscratch) },
     (0x341,  _) => { Some(set_xret_target(Machine, value)) },
@@ -161,7 +161,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x104,  _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits) },
     (0x105,  _) => { Some(set_stvec(value)) },
     (0x106,  _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits)) },
-    (0x10A,  _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) },
+    (0x10A,  _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) },
     (0x140,  _) => { sscratch = value; Some(sscratch) },
     (0x141,  _) => { Some(set_xret_target(Supervisor, value)) },
     (0x142,  _) => { scause.bits = value; Some(scause.bits) },