Add support for Zcmt extension

c_emulator/riscv_platform.c

@@ -37,6 +37,16 @@ bool sys_enable_zcb(unit u)
   return rv_enable_zcb;
 }
 
+bool sys_enable_zcd(unit u)
+{
+  return rv_enable_zcd;
+}
+
+bool sys_enable_zcmt(unit u)
+{
+  return rv_enable_zcmt;
+}
+
 bool sys_enable_zfinx(unit u)
 {
   return rv_enable_zfinx;

c_emulator/riscv_platform.h

@@ -5,6 +5,8 @@ bool sys_enable_rvc(unit);
 bool sys_enable_fdext(unit);
 bool sys_enable_svinval(unit);
 bool sys_enable_zcb(unit);
+bool sys_enable_zcd(unit);
+bool sys_enable_zcmt(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);

c_emulator/riscv_platform_impl.c

@@ -11,6 +11,8 @@ uint64_t rv_vector_elen_exp = 0x6;
 
 bool rv_enable_svinval = false;
 bool rv_enable_zcb = false;
+bool rv_enable_zcd = true;
+bool rv_enable_zcmt = false;
 bool rv_enable_zfinx = false;
 bool rv_enable_rvc = true;
 bool rv_enable_writable_misa = true;

c_emulator/riscv_platform_impl.h

@@ -16,6 +16,8 @@ extern uint64_t rv_vector_elen_exp;
 
 extern bool rv_enable_svinval;
 extern bool rv_enable_zcb;
+extern bool rv_enable_zcd;
+extern bool rv_enable_zcmt;
 extern bool rv_enable_zfinx;
 extern bool rv_enable_rvc;
 extern bool rv_enable_fdext;

c_emulator/riscv_sim.c

@@ -50,6 +50,7 @@ enum {
   OPT_PMP_GRAIN,
   OPT_ENABLE_SVINVAL,
   OPT_ENABLE_ZCB,
+  OPT_ENABLE_ZCMT,
   OPT_ENABLE_ZICBOM,
   OPT_ENABLE_ZICBOZ,
   OPT_ENABLE_SSTC,
@@ -148,6 +149,7 @@ static struct option options[] = {
     {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},
     {"enable-svinval",              no_argument,       0, OPT_ENABLE_SVINVAL      },
     {"enable-zcb",                  no_argument,       0, OPT_ENABLE_ZCB          },
+    {"enable-zcmt",                 no_argument,       0, OPT_ENABLE_ZCMT         },
     {"enable-zicbom",               no_argument,       0, OPT_ENABLE_ZICBOM       },
     {"enable-zicboz",               no_argument,       0, OPT_ENABLE_ZICBOZ       },
     {"cache-block-size",            required_argument, 0, OPT_CACHE_BLOCK_SIZE    },
@@ -387,6 +389,10 @@ static int process_args(int argc, char **argv)
     case OPT_ENABLE_ZCB:
       fprintf(stderr, "enabling Zcb extension.\n");
       rv_enable_zcb = true;
+    case OPT_ENABLE_ZCMT:
+      fprintf(stderr, "enabling Zcmt extension.\n");
+      rv_enable_zcd = false;
+      rv_enable_zcmt = true;
       break;
     case OPT_ENABLE_ZICBOM:
       fprintf(stderr, "enabling Zicbom extension.\n");

model/CMakeLists.txt

@@ -66,6 +66,7 @@ foreach (xlen IN ITEMS 32 64)
                 "riscv_insts_zbc.sail"
                 "riscv_insts_zbs.sail"
                 "riscv_insts_zcb.sail"
+                "riscv_insts_zcmt.sail"
                 "riscv_insts_zfh.sail"
                 # Zfa needs to be added after fext, dext and Zfh (as it needs
                 # definitions from those)

model/riscv_addr_checks.sail

@@ -59,6 +59,11 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex
   let addr = virtaddr(X(base) + offset) in
   Ext_DataAddr_OK(addr)
 
+function ext_data_get_addr_from_bits(addr_ext : xlenbits, acc : AccessType(ext_access_type), width : mem_access_width)
+         -> Ext_DataAddr_Check(ext_data_addr_error) =
+  let addr = virtaddr(addr_ext) in
+  Ext_DataAddr_OK(addr)
+
 function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
   ()
 

model/riscv_extensions.sail

@@ -67,6 +67,8 @@ enum clause extension = Ext_Zdinx
 enum clause extension = Ext_Zca
 // Code Size Reduction: additional 16-bit aliases
 enum clause extension = Ext_Zcb
+// Code Size Reduction: compressed table jump instructions
+enum clause extension = Ext_Zcmt
 // Code Size Reduction: compressed double precision floating point loads and stores
 enum clause extension = Ext_Zcd
 // Code Size Reduction: compressed single precision floating point loads and stores

model/riscv_insts_zcd.sail

@@ -6,7 +6,7 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-function clause extensionEnabled(Ext_Zcd) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_D) & (xlen == 32 | xlen == 64)
+function clause extensionEnabled(Ext_Zcd) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_D) & sys_enable_zcd() & not(sys_enable_zcmt()) & (xlen == 32 | xlen == 64)
 
 union clause ast = C_FLDSP : (bits(6), regidx)
 

model/riscv_insts_zcmt.sail

@@ -0,0 +1,95 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+function clause extensionEnabled(Ext_Zcmt) = extensionEnabled(Ext_Zca) & sys_enable_zcmt() & not(sys_enable_zcd()) & (xlen == 32 | xlen == 64)
+
+type target_address = bits(xlen)
+
+union FJT_Result = {
+  FJT_Success : target_address,
+  FJT_Failure : unit
+}
+
+function fetch_jump_table(table_address : bits(xlen)) -> FJT_Result = {
+    /* Fetching jump table address needs execute permission */
+    match ext_data_get_addr_from_bits(table_address, Execute(), xlen_bytes) {
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); FJT_Failure() },
+    Ext_DataAddr_OK(vaddr) => {
+      if   check_misaligned(vaddr, size_bytes(xlen_bytes))
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); FJT_Failure() }
+      else match translateAddr(vaddr, Execute()) {
+        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); FJT_Failure() },
+        TR_Address(paddr, _) =>
+          match mem_read(Execute(), paddr, xlen_bytes, false, false, false) {
+            Ok(result) => { FJT_Success(result) },
+            Err(e)     => { handle_mem_exception(vaddr, e); FJT_Failure() },
+          },
+      }
+    },
+  };
+}
+
+union clause ast = CM_JALT : (bits(8))
+
+mapping clause encdec_compressed = CM_JALT(index) if extensionEnabled(Ext_Zcmt) & 32 <= unsigned(index)
+  <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 if extensionEnabled(Ext_Zcmt) & 32 <= unsigned(index)
+
+function clause execute (CM_JALT(index)) = {
+  let base : bits(xlen) = jvt.bits & ~(zero_extend(0x3F)); 
+  let index : bits(xlen) = zero_extend(index);
+  if jvt[mode] == 0b000000 then {
+    let table_address : bits(xlen) = match xlen {
+      32 => base + index << 2,
+      64 => base + index << 3,
+       _ => internal_error(__FILE__, __LINE__, "Unsupported xlen")
+    };
+    match fetch_jump_table(table_address) {
+        FJT_Failure(_) => { 
+          return RETIRE_FAIL 
+        },
+        FJT_Success(target_address) => { 
+          X(0b00001) = get_next_pc(); 
+          set_next_pc(target_address & ~(zero_extend(0x1)));
+        }
+    };
+  };
+  RETIRE_SUCCESS
+}
+
+mapping clause assembly = CM_JALT(index) if (xlen == 32 | xlen == 64) <->
+  "cm.jalt" ^ spc() ^ hex_bits_8(index) if (xlen == 32 | xlen == 64)
+
+/* ****************************************************************** */
+union clause ast = CM_JT : (bits(8))
+
+mapping clause encdec_compressed = CM_JT(index) if extensionEnabled(Ext_Zcmt) & unsigned(index) < 32
+  <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 if extensionEnabled(Ext_Zcmt) & unsigned(index) < 32
+
+function clause execute (CM_JT(index)) = {
+  let base : bits(xlen) = jvt.bits & ~(zero_extend(0x3F)); 
+  let index : bits(xlen) = zero_extend(index);
+  if jvt[mode] == 0b000000 then {
+    let table_address : bits(xlen) = match xlen {
+      32 => base + index << 2,
+      64 => base + index << 3,
+       _ => internal_error(__FILE__, __LINE__, "Unsupported xlen")
+    };
+    match fetch_jump_table(table_address) {
+        FJT_Failure(_) => { 
+          return RETIRE_FAIL 
+        },
+        FJT_Success(target_address) => { 
+          set_next_pc(target_address & ~(zero_extend(0x1))); 
+        }
+    };
+  };
+  RETIRE_SUCCESS
+}
+
+mapping clause assembly = CM_JT(index) if (xlen == 32 | xlen == 64) <->
+  "cm.jt" ^ spc() ^ hex_bits_8(index) if (xlen == 32 | xlen == 64)

model/riscv_sys_regs.sail

@@ -92,6 +92,10 @@ val sys_enable_fdext = pure "sys_enable_fdext" : unit -> bool
 val sys_enable_svinval = pure "sys_enable_svinval" : unit -> bool
 /* whether Zcb was enabled at boot */
 val sys_enable_zcb = pure "sys_enable_zcb" : unit -> bool
+/* whether Zcd was enabled at boot */
+val sys_enable_zcd = pure "sys_enable_zcd" : unit -> bool
+/* whether Zcmt was enabled at boot */
+val sys_enable_zcmt = pure "sys_enable_zcmt" : unit -> bool
 /* whether zfinx was enabled at boot */
 val sys_enable_zfinx = pure "sys_enable_zfinx" : unit -> bool
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
@@ -508,6 +512,16 @@ function clause write_CSR((0x302, value) if xlen == 32) = { medeleg = legalize_m
 function clause write_CSR((0x312, value) if xlen == 32) = { medeleg = legalize_medeleg(medeleg, value @ medeleg.bits[31 .. 0]); medeleg.bits[63 .. 32] }
 function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
 
+bitfield Jvt : xlenbits = {
+  base : xlen - 1 .. 6,
+  mode : 5 .. 0
+}
+register jvt : Jvt
+mapping clause csr_name_map = 0x017  <-> "jvt"
+function clause is_CSR_defined (0x017) = sys_enable_zcmt()
+function clause write_CSR(0x017, value) = { jvt.bits = (value >> 6 ) << 6; jvt.bits }
+function clause read_CSR(0x017) = jvt.bits
+
 /* registers for trap handling */
 
 bitfield Mtvec : xlenbits = {
@@ -902,6 +916,9 @@ function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
 
 /*
  * Entropy Source - Platform access to random bits.
+ * WARNING: This function currently lacks a proper side-effect annotation.
+ *          If you are using theorem prover tool flows, you
+ *          may need to modify or stub out this function for now.
  * NOTE: This would be better placed in riscv_platform.sail, but that file
  *       appears _after_ this one in the compile order meaning the valspec
  *       for this function is unavailable when it's first encountered in

model/riscv_termination.sail

@@ -56,6 +56,7 @@ function extensionEnabled_measure(ext : extension) -> int =
     Ext_Zcb => 2, // Ext_Zca
     Ext_Zcd => 2, // Ext_Zca, (Ext_D)
     Ext_Zcf => 2, // Ext_Zca, (Ext_F)
+    Ext_Zcmt => 2, // Ext_Zcmt
     _ => 0
   }
 termination_measure extensionEnabled(ext) = extensionEnabled_measure(ext)