From 965866c5a067b7555b44b701df1c589209b6622d Mon Sep 17 00:00:00 2001
From: sanket <telisanket2002@gmail.com>
Date: Sat, 20 Jan 2024 20:30:32 +0530
Subject: [PATCH] Use "extensionEnabled" function for C extension

---
 model/riscv_fetch.sail       |   2 +-
 model/riscv_fetch_rvfi.sail  |   2 +-
 model/riscv_insts_base.sail  |   6 +-
 model/riscv_insts_cdext.sail |  16 ++---
 model/riscv_insts_cext.sail  | 134 ++++++++++++++++++-----------------
 model/riscv_insts_cfext.sail |  16 ++---
 model/riscv_jalr_seq.sail    |   2 +-
 model/riscv_step.sail        |   2 +-
 model/riscv_sys_regs.sail    |   1 -
 9 files changed, 92 insertions(+), 89 deletions(-)

diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 6fd66917d..78401c8b8 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -19,7 +19,7 @@ function fetch() -> FetchResult =
   match ext_fetch_check_pc(PC, PC) {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_C))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _)     => F_Error(e, PC),
diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
index d25237572..cdb8f9416 100644
--- a/model/riscv_fetch_rvfi.sail
+++ b/model/riscv_fetch_rvfi.sail
@@ -17,7 +17,7 @@ function fetch() -> FetchResult = {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
       /* then check PC alignment */
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_C))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _) => F_Error(e, PC),
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 26915f22c..95d3f785f 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -9,6 +9,8 @@
 /* ****************************************************************** */
 /* This file specifies the instructions in the base integer set.      */
 
+enum clause extension = Ext_C
+function clause extensionEnabled(Ext_C) = misa[C] == 0b1
 
 /* ****************************************************************** */
 union clause ast = UTYPE : (bits(20), regidx, uop)
@@ -67,7 +69,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     },
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
-      if bit_to_bool(target[1]) & not(haveRVC())
+      if bit_to_bool(target[1]) & not(extensionEnabled(Ext_C))
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
@@ -131,7 +133,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
         RETIRE_FAIL
       },
       Ext_ControlAddr_OK(target) => {
-        if bit_to_bool(target[1]) & not(haveRVC()) then {
+        if bit_to_bool(target[1]) & not(extensionEnabled(Ext_C)) then {
           handle_mem_exception(target, E_Fetch_Addr_Align());
           RETIRE_FAIL;
         } else {
diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail
index 6412d781b..5571befd4 100644
--- a/model/riscv_insts_cdext.sail
+++ b/model/riscv_insts_cdext.sail
@@ -17,9 +17,9 @@
 union clause ast = C_FLDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
   <-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
 
 function clause execute (C_FLDSP(uimm, rd)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -35,9 +35,9 @@ mapping clause assembly = C_FLDSP(uimm, rd)
 union clause ast = C_FSDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
   <-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
 
 function clause execute (C_FSDSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -53,9 +53,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2)
 union clause ast = C_FLD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
   <-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
 
 function clause execute (C_FLD(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -73,9 +73,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc)
 union clause ast = C_FSD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
   <-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D)
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extensionEnabled(Ext_C) & extensionEnabled(Ext_D)
 
 function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index b7c63c2a5..c93332a1d 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -17,8 +17,8 @@
 /* ****************************************************************** */
 union clause ast = C_NOP : unit
 
-mapping clause encdec_compressed = C_NOP()
-  <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01
+mapping clause encdec_compressed = C_NOP() if extensionEnabled(Ext_C)
+  <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute C_NOP() = RETIRE_SUCCESS
 
@@ -29,9 +29,9 @@ mapping clause assembly = C_NOP() <-> "c.nop"
 union clause ast = C_ADDI4SPN : (cregidx, bits(8))
 
 mapping clause encdec_compressed = C_ADDI4SPN(rd, nz96 @ nz54 @ nz3 @ nz2)
-      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000
+      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 & extensionEnabled(Ext_C)
   <-> 0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregidx @ 0b00
-      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000
+      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 & extensionEnabled(Ext_C)
 
 function clause execute (C_ADDI4SPN(rdc, nzimm)) = {
   let imm : bits(12) = (0b00 @ nzimm @ 0b00);
@@ -47,8 +47,8 @@ mapping clause assembly = C_ADDI4SPN(rdc, nzimm)
 /* ****************************************************************** */
 union clause ast = C_LW : (bits(5), cregidx, cregidx)
 
-mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd)
-  <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
+mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd) if extensionEnabled(Ext_C)
+  <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 if extensionEnabled(Ext_C)
 
 function clause execute (C_LW(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -64,9 +64,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc)
 union clause ast = C_LD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_LD(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -83,8 +83,8 @@ mapping clause assembly = C_LD(uimm, rsc, rdc)
 /* ****************************************************************** */
 union clause ast = C_SW : (bits(5), cregidx, cregidx)
 
-mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2)
-  <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
+mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2) if extensionEnabled(Ext_C)
+  <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 if extensionEnabled(Ext_C)
 
 function clause execute (C_SW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -100,9 +100,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2)
 union clause ast = C_SD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_SD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -120,9 +120,9 @@ mapping clause assembly = C_SD(uimm, rsc1, rsc2)
 union clause ast = C_ADDI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_ADDI(nzi5 @ nzi40, rsd)
-      if nzi5 @ nzi40 != 0b000000 & rsd != zreg
+      if nzi5 @ nzi40 != 0b000000 & rsd != zreg & extensionEnabled(Ext_C)
   <-> 0b000 @ nzi5 : bits(1) @ rsd : regidx @ nzi40 : bits(5) @ 0b01
-      if nzi5 @ nzi40 != 0b000000 & rsd != zreg
+      if nzi5 @ nzi40 != 0b000000 & rsd != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_ADDI(nzi, rsd)) = {
   let imm : bits(12) = sign_extend(nzi);
@@ -138,9 +138,9 @@ mapping clause assembly = C_ADDI(nzi, rsd)
 union clause ast = C_JAL : (bits(11))
 
 mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31)
-      if sizeof(xlen) == 32
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C)
   <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01
-      if sizeof(xlen) == 32
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C)
 
 function clause execute (C_JAL(imm)) =
   execute(RISCV_JAL(sign_extend(imm @ 0b0), ra))
@@ -154,9 +154,9 @@ mapping clause assembly = C_JAL(imm)
 union clause ast = C_ADDIW : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
-      if rsd != zreg & sizeof(xlen) == 64
+      if rsd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b001 @ imm5 : bits(1) @ rsd : regidx @ imm40 : bits(5) @ 0b01
-      if rsd != zreg & sizeof(xlen) == 64
+      if rsd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_ADDIW(imm, rsd)) =
   execute(ADDIW(sign_extend(imm), rsd, rsd))
@@ -170,9 +170,9 @@ mapping clause assembly = C_ADDIW(imm, rsd)
 union clause ast = C_LI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LI(imm5 @ imm40, rd)
-      if rd != zreg
+      if rd != zreg & extensionEnabled(Ext_C)
   <-> 0b010 @ imm5 : bits(1) @ rd : regidx @ imm40 : bits(5) @ 0b01
-      if rd != zreg
+      if rd != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_LI(imm, rd)) = {
   let imm : bits(12) = sign_extend(imm);
@@ -188,9 +188,9 @@ mapping clause assembly = C_LI(imm, rd)
 union clause ast = C_ADDI16SP : (bits(6))
 
 mapping clause encdec_compressed = C_ADDI16SP(nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4)
-      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000
+      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 & extensionEnabled(Ext_C)
   <-> 0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01
-      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000
+      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 & extensionEnabled(Ext_C)
 
 function clause execute (C_ADDI16SP(imm)) = {
   let imm : bits(12) = sign_extend(imm @ 0x0);
@@ -206,9 +206,9 @@ mapping clause assembly = C_ADDI16SP(imm)
 union clause ast = C_LUI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LUI(imm17 @ imm1612, rd)
-      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000
+      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 & extensionEnabled(Ext_C)
   <-> 0b011 @ imm17 : bits(1) @ rd : regidx @ imm1612 : bits(5) @ 0b01
-      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000
+      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 & extensionEnabled(Ext_C)
 
 function clause execute (C_LUI(imm, rd)) = {
   let res : bits(20) = sign_extend(imm);
@@ -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 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C)
   <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
-      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C)
 
 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 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C)
   <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
-      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C)
 
 function clause execute (C_SRAI(shamt, rsd)) = {
   let rsd = creg2reg_idx(rsd);
@@ -259,8 +259,8 @@ mapping clause assembly = C_SRAI(shamt, rsd)
 /* ****************************************************************** */
 union clause ast = C_ANDI : (bits(6), cregidx)
 
-mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd)
-  <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01
+mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd) if extensionEnabled(Ext_C)
+  <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_ANDI(imm, rsd)) = {
   let rsd = creg2reg_idx(rsd);
@@ -273,8 +273,8 @@ mapping clause assembly = C_ANDI(imm, rsd)
 /* ****************************************************************** */
 union clause ast = C_SUB : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_SUB(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_SUB(rsd, rs2) if extensionEnabled(Ext_C)
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_SUB(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -288,8 +288,8 @@ mapping clause assembly = C_SUB(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_XOR : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_XOR(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_XOR(rsd, rs2) if extensionEnabled(Ext_C)
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_XOR(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -303,8 +303,8 @@ mapping clause assembly = C_XOR(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_OR : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_OR(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_OR(rsd, rs2) if extensionEnabled(Ext_C)
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_OR(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -318,8 +318,8 @@ mapping clause assembly = C_OR(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_AND : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_AND(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_AND(rsd, rs2) if extensionEnabled(Ext_C)
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_AND(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -334,9 +334,9 @@ mapping clause assembly = C_AND(rsd, rs2)
 union clause ast = C_SUBW : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SUBW(rsd, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_SUBW(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -353,9 +353,9 @@ mapping clause assembly = C_SUBW(rsd, rs2)
 union clause ast = C_ADDW : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_ADDW(rsd, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_ADDW(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -371,8 +371,8 @@ mapping clause assembly = C_ADDW(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_J : (bits(11))
 
-mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31)
-  <-> 0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01
+mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) if extensionEnabled(Ext_C)
+  <-> 0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_J(imm)) =
   execute(RISCV_JAL(sign_extend(imm @ 0b0), zreg))
@@ -383,8 +383,8 @@ mapping clause assembly = C_J(imm)
 /* ****************************************************************** */
 union clause ast = C_BEQZ : (bits(8), cregidx)
 
-mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs)
-  <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
+mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs) if extensionEnabled(Ext_C)
+  <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_BEQZ(imm, rs)) =
   execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ))
@@ -395,8 +395,8 @@ mapping clause assembly = C_BEQZ(imm, rs)
 /* ****************************************************************** */
 union clause ast = C_BNEZ : (bits(8), cregidx)
 
-mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs)
-  <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
+mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs) if extensionEnabled(Ext_C)
+  <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 if extensionEnabled(Ext_C)
 
 function clause execute (C_BNEZ(imm, rs)) =
   execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE))
@@ -408,9 +408,9 @@ mapping clause assembly = C_BNEZ(imm, rs)
 union clause ast = C_SLLI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C)
   <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10
-      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C)
 
 function clause execute (C_SLLI(shamt, rsd)) =
   execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))
@@ -424,9 +424,9 @@ mapping clause assembly = C_SLLI(shamt, rsd)
 union clause ast = C_LWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd)
-      if rd != zreg
+      if rd != zreg & extensionEnabled(Ext_C)
   <-> 0b010 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
-      if rd != zreg
+      if rd != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_LWSP(uimm, rd)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -442,9 +442,9 @@ mapping clause assembly = C_LWSP(uimm, rd)
 union clause ast = C_LDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd)
-      if rd != zreg & sizeof(xlen) == 64
+      if rd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if rd != zreg & sizeof(xlen) == 64
+      if rd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_LDSP(uimm, rd)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -460,7 +460,9 @@ mapping clause assembly = C_LDSP(uimm, rd)
 union clause ast = C_SWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SWSP(ui76 @ ui52, rs2)
+      if extensionEnabled(Ext_C)
   <-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
+      if extensionEnabled(Ext_C)
 
 function clause execute (C_SWSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -474,9 +476,9 @@ mapping clause assembly = C_SWSP(uimm, rs2)
 union clause ast = C_SDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
   <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_C)
 
 function clause execute (C_SDSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -492,9 +494,9 @@ mapping clause assembly = C_SDSP(uimm, rs2)
 union clause ast = C_JR : (regidx)
 
 mapping clause encdec_compressed = C_JR(rs1)
-      if rs1 != zreg
+      if rs1 != zreg & extensionEnabled(Ext_C)
   <-> 0b100 @ 0b0 @ rs1 : regidx @ 0b00000 @ 0b10
-      if rs1 != zreg
+      if rs1 != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_JR(rs1)) =
   execute(RISCV_JALR(zero_extend(0b0), rs1, zreg))
@@ -508,9 +510,9 @@ mapping clause assembly = C_JR(rs1)
 union clause ast = C_JALR : (regidx)
 
 mapping clause encdec_compressed = C_JALR(rs1)
-      if rs1 != zreg
+      if rs1 != zreg & extensionEnabled(Ext_C)
   <-> 0b100 @ 0b1 @ rs1 : regidx @ 0b00000 @ 0b10
-      if rs1 != zreg
+      if rs1 != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_JALR(rs1)) =
   execute(RISCV_JALR(zero_extend(0b0), rs1, ra))
@@ -524,9 +526,9 @@ mapping clause assembly = C_JALR(rs1)
 union clause ast = C_MV : (regidx, regidx)
 
 mapping clause encdec_compressed = C_MV(rd, rs2)
-      if rd != zreg & rs2 != zreg
+      if rd != zreg & rs2 != zreg & extensionEnabled(Ext_C)
   <-> 0b100 @ 0b0 @ rd : regidx @ rs2 : regidx @ 0b10
-      if rd != zreg & rs2 != zreg
+      if rd != zreg & rs2 != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_MV(rd, rs2)) =
   execute(RTYPE(rs2, zreg, rd, RISCV_ADD))
@@ -539,8 +541,8 @@ mapping clause assembly = C_MV(rd, rs2)
 /* ****************************************************************** */
 union clause ast = C_EBREAK : unit
 
-mapping clause encdec_compressed = C_EBREAK()
-  <-> 0b100 @ 0b1 @ 0b00000 @ 0b00000 @ 0b10
+mapping clause encdec_compressed = C_EBREAK() if extensionEnabled(Ext_C)
+  <-> 0b100 @ 0b1 @ 0b00000 @ 0b00000 @ 0b10 if extensionEnabled(Ext_C)
 
 function clause execute C_EBREAK() =
   execute(EBREAK())
@@ -551,9 +553,9 @@ mapping clause assembly = C_EBREAK() <-> "c.ebreak"
 union clause ast = C_ADD : (regidx, regidx)
 
 mapping clause encdec_compressed = C_ADD(rsd, rs2)
-      if rsd != zreg & rs2 != zreg
+      if rsd != zreg & rs2 != zreg & extensionEnabled(Ext_C)
   <-> 0b100 @ 0b1 @ rsd : regidx @ rs2 : regidx @ 0b10
-      if rsd != zreg & rs2 != zreg
+      if rsd != zreg & rs2 != zreg & extensionEnabled(Ext_C)
 
 function clause execute (C_ADD(rsd, rs2)) =
   execute(RTYPE(rs2, rsd, rsd, RISCV_ADD))
diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail
index 3787e2420..976425d53 100644
--- a/model/riscv_insts_cfext.sail
+++ b/model/riscv_insts_cfext.sail
@@ -17,9 +17,9 @@
 union clause ast = C_FLWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd)
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
   <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
 
 function clause execute (C_FLWSP(imm, rd)) = {
   let imm : bits(12) = zero_extend(imm @ 0b00);
@@ -35,9 +35,9 @@ mapping clause assembly = C_FLWSP(imm, rd)
 union clause ast = C_FSWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
   <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
 
 function clause execute (C_FSWSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -53,9 +53,9 @@ mapping clause assembly = C_FSWSP(uimm, rs2)
 union clause ast = C_FLW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd)
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
 
 function clause execute (C_FLW(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -73,9 +73,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc)
 union clause ast = C_FSW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
   <-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F)
+      if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F)
 
 function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 497a44178..0f4abd0e9 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -24,7 +24,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
     },
     Ext_ControlAddr_OK(addr) => {
       let target = [addr with 0 = bitzero];  /* clear addr[0] */
-      if bit_to_bool(target[1]) & not(haveRVC()) then {
+      if bit_to_bool(target[1]) & not(extensionEnabled(Ext_C)) then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 5ff7e4bc0..6f2a15862 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -54,7 +54,7 @@ function step(step_no : int) -> bool = {
               print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
             };
             /* check for RVC once here instead of every RVC execute clause. */
-            if haveRVC() then {
+            if extensionEnabled(Ext_C) then {
               nextPC = PC + 2;
               (execute(ast), true)
             } else {
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 76e684d35..58f5e91dc 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -131,7 +131,6 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
 /* helpers to check support for various extensions. */
 /* we currently don't model 'E', so always assume 'I'. */
 function haveAtomics() -> bool = misa[A] == 0b1
-function haveRVC()     -> bool = misa[C] == 0b1
 function haveMulDiv()  -> bool = misa[M] == 0b1
 function haveSupMode() -> bool = misa[S] == 0b1
 function haveUsrMode() -> bool = misa[U] == 0b1