Add support for Zcmt extension

README.md

@@ -109,7 +109,7 @@ Supported RISC-V ISA features
 - Zfa extension for additional floating-point instructions, v1.0
 - Zfinx, Zdinx, and Zhinx extensions for floating-point in integer registers, v1.0
 - C extension for compressed instructions, v2.0
-- Zca, Zcf, Zcd, and Zcb extensions for code size reduction, v1.0
+- Zca, Zcf, Zcd, Zcb, and Zcmt extensions for code size reduction, v1.0
 - Zcmop extension for compressed May-Be-Operations, v1.0
 - B (Zba, Zbb, Zbs) and Zbc extensions for bit manipulation, v1.0
 - Zbkb, Zbkc, and Zbkx extensions for bit manipulation for cryptography, v1.0

config/default.json

@@ -119,6 +119,9 @@
         "Zcb" : {
             "supported" : true
         },
+        "Zcmt" : {
+            "supported" : false
+        },
         "Zcmop" : {
             "supported" : true
         },

model/CMakeLists.txt

@@ -72,6 +72,7 @@ foreach (xlen IN ITEMS 32 64)
                 "riscv_insts_zba.sail"
                 "riscv_insts_zbb.sail"
                 "riscv_insts_zbc.sail"
+                "riscv_insts_zcmt.sail"
                 "riscv_insts_zbs.sail"
                 "riscv_insts_zcb.sail"
                 "riscv_insts_zfh.sail"

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

@@ -108,6 +108,9 @@ function clause hartSupports(Ext_Zca) = config extensions.Zca.supported
 // Code Size Reduction: additional 16-bit aliases
 enum clause extension = Ext_Zcb
 function clause hartSupports(Ext_Zcb) = config extensions.Zcb.supported
+// Code Size Reduction: compressed table jump instructions
+enum clause extension = Ext_Zcmt
+function clause hartSupports(Ext_Zcmt) = config extensions.Zcmt.supported
 // Code Size Reduction: compressed double precision floating point loads and stores
 enum clause extension = Ext_Zcd
 function clause hartSupports(Ext_Zcd) = config extensions.Zcd.supported

model/riscv_insts_zcd.sail

@@ -6,7 +6,7 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-function clause currentlyEnabled(Ext_Zcd) = hartSupports(Ext_Zcd) & currentlyEnabled(Ext_D) & currentlyEnabled(Ext_Zca) & (currentlyEnabled(Ext_C) | not(hartSupports(Ext_C)))
+function clause currentlyEnabled(Ext_Zcd) = hartSupports(Ext_Zcd) & currentlyEnabled(Ext_D) & currentlyEnabled(Ext_Zca) & not(currentlyEnabled(Ext_Zcmt)) & (currentlyEnabled(Ext_C) | not(hartSupports(Ext_C)))
 
 union clause ast = C_FLDSP : (bits(6), fregidx)
 

model/riscv_insts_zcmt.sail

@@ -0,0 +1,86 @@
+/*=======================================================================================*/
+/*  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 currentlyEnabled(Ext_Zcmt) = hartSupports(Ext_Zcmt) & currentlyEnabled(Ext_Zca) & not(currentlyEnabled(Ext_Zcd))
+
+type target_address = xlenbits
+
+function fetch_jump_table(table_address : xlenbits) -> result(target_address, unit) = {
+  /* Executable permission required to fetch jump table address */
+  match ext_data_get_addr_from_bits(table_address, Execute(), xlen_bytes) {
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); Err() },
+    Ext_DataAddr_OK(vaddr) => {
+      if   check_misaligned(vaddr, size_bytes(xlen_bytes))
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); Err() }
+      else match translateAddr(vaddr, Execute()) {
+        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); Err() },
+        TR_Address(paddr, _) =>
+          match mem_read(Execute(), paddr, xlen_bytes, false, false, false) {
+            Ok(result) => { Ok(result) },
+            Err(e)     => { handle_mem_exception(vaddr, e); Err() },
+          }
+      }
+    }
+  }
+}
+
+union clause ast = CM_JALT : (bits(8))
+
+mapping clause encdec_compressed = CM_JALT(index)
+  <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10
+  when currentlyEnabled(Ext_Zcmt) & 32 <= unsigned(index)
+
+function clause execute (CM_JALT(index)) = {
+  let base  : bits(xlen) = jvt[base] @ 0b000000;
+  let index : bits(xlen) = zero_extend(index);
+  if jvt[mode] == 0b000000 then {
+    let table_address = base + (index << log2_xlen_bytes);
+    match fetch_jump_table(table_address) {
+        Err(_) => { RETIRE_FAIL },
+        Ok(target_address) => {
+          X(ra) = get_next_pc();
+          set_next_pc([target_address with 0 = bitzero]);
+          RETIRE_SUCCESS
+        }
+    };
+  } else {
+    handle_illegal();
+    RETIRE_FAIL
+  };
+}
+
+mapping clause assembly = CM_JALT(index)
+   <-> "cm.jalt" ^ spc() ^ hex_bits_8(index)
+
+/* ****************************************************************** */
+union clause ast = CM_JT : (bits(8))
+
+mapping clause encdec_compressed = CM_JT(index)
+  <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10
+  when currentlyEnabled(Ext_Zcmt) & unsigned(index) < 32
+
+function clause execute (CM_JT(index)) = {
+  let base  : bits(xlen) = jvt[base] @ 0b000000;
+  let index : bits(xlen) = zero_extend(index);
+  if jvt[mode] == 0b000000 then {
+    let table_address = base + (index << log2_xlen_bytes);
+    match fetch_jump_table(table_address) {
+        Err(_) => { RETIRE_FAIL },
+        Ok(target_address) => {
+          set_next_pc([target_address with 0 = bitzero]);
+          RETIRE_SUCCESS
+        }
+    };
+  } else {
+      handle_illegal();
+      RETIRE_FAIL
+    };
+}
+
+mapping clause assembly = CM_JT(index)
+  <-> "cm.jt" ^ spc() ^ hex_bits_8(index)

model/riscv_sys_regs.sail

@@ -978,3 +978,24 @@ function get_vtype_vma() = decode_agtype(vtype[vma])
 
 val get_vtype_vta : unit -> agtype
 function get_vtype_vta() = decode_agtype(vtype[vta])
+
+/* Zcmt register */
+
+bitfield Jvt : xlenbits = {
+  base : xlen - 1 .. 6,
+  mode : 5 .. 0
+}
+register jvt : Jvt
+
+function legalize_jvt(o : Jvt, v : xlenbits) -> Jvt = {
+  let v = Mk_Jvt(v);
+  [o with
+    base = v[base],
+    mode = 0b000000
+  ]
+}
+
+mapping clause csr_name_map = 0x017  <-> "jvt"
+function clause is_CSR_defined (0x017) = currentlyEnabled(Ext_Zcmt)
+function clause write_CSR(0x017, value) = { jvt = legalize_jvt(jvt, value); jvt.bits }
+function clause read_CSR(0x017) = jvt.bits