diff --git a/model/riscv_insts_zvkb.sail b/model/riscv_insts_zvkb.sail
index c8a167475..deed76b19 100644
--- a/model/riscv_insts_zvkb.sail
+++ b/model/riscv_insts_zvkb.sail
@@ -3,6 +3,20 @@
  * ----------------------------------------------------------------------
  */
 
+/*
+ * Helper functions
+ * ----------------------------------------------------------------------
+ */
+
+val	 clmul : forall 'm, 'm >= 0. (bits('m), bits('m)) -> bits('m)
+function clmul(x, y) = {
+    result : bits('m) = zeros();
+    foreach (i from 0 to ('m - 1)) {
+      if y[i] == 0x1[1] then result = result ^ (x << i);
+    };
+    result
+}
+
 /* VROL.VV */
 
 union clause ast = RISCV_VROL_VV : (bits(1), regidx, regidx, regidx)
@@ -395,3 +409,99 @@ function clause execute (RISCV_VANDN_VX(vm, rs1, vs2, vd)) = {
   vstart = EXTZ(0b0);
   RETIRE_SUCCESS
 }
+
+/* VCLMUL.VV */
+
+union clause ast = RISCV_VCLMUL_VV : (bits(1), regidx, regidx, regidx)
+
+mapping clause encdec = RISCV_VCLMUL_VV(vm, vs1, vs2, vd) if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+ <-> 0b001100 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111   if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+
+mapping clause assembly = RISCV_VCLMUL_VV(vm, vs1, vs2, vd)
+ <-> "vclmul.vv" ^ spc() ^ vreg_name(vd)
+		 ^ sep() ^ vreg_name(vs2)
+		 ^ sep() ^ vreg_name(vs1)
+		 ^ maybe_vmask(vm)
+
+function clause execute (RISCV_VCLMUL_VV(vm, vs1, vs2, vd)) = {
+  let SEW      = get_sew();
+  let LMUL_pow = get_lmul_pow();
+  let VLEN     = int_power(2, get_vlen_pow());
+  let num_elem = get_num_elem(LMUL_pow, SEW);
+
+  let 'n = num_elem;
+  let 'm = SEW;
+  assert('m == 64);
+  assert(sizeof(xlen) == 64);
+
+  let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, vreg_name("v0"));
+  let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
+  let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
+  let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
+  result      : vector('n, dec, bits('m)) = undefined;
+  mask        : vector('n, dec, bool)     = undefined;
+
+  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+
+  foreach (i from unsigned(vstart) to (unsigned(vl) - 1)) {
+    assert(0 <= i & i < 'n);
+    if mask[i] then {
+      let op1	  : bits(64) = vs2_val[i];
+      let op2	  : bits(64) = vs1_val[i];
+      let product : bits(64) = clmul(op1, op2);
+      result[i] = ~(op1) & op2;
+    };
+  };
+
+  write_single_vreg(num_elem, 'm, vd, result);
+  vstart = EXTZ(0b0);
+  RETIRE_SUCCESS
+}
+
+/* VCLMUL.VX */
+
+union clause ast = RISCV_VCLMUL_VX : (bits(1), regidx, regidx, regidx)
+
+mapping clause encdec = RISCV_VCLMUL_VX(vm, rs1, vs2, vd) if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+ <-> 0b001100 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111   if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+
+mapping clause assembly = RISCV_VCLMUL_VX(vm, rs1, vs2, vd)
+ <-> "vclmul.vv" ^ spc() ^ vreg_name(vd)
+		 ^ sep() ^ vreg_name(vs2)
+		 ^ sep() ^ reg_name(rs1)
+		 ^ maybe_vmask(vm)
+
+function clause execute (RISCV_VCLMUL_VX(vm, rs1, vs2, vd)) = {
+  let SEW      = get_sew();
+  let LMUL_pow = get_lmul_pow();
+  let VLEN     = int_power(2, get_vlen_pow());
+  let num_elem = get_num_elem(LMUL_pow, SEW);
+
+  let 'n = num_elem;
+  let 'm = SEW;
+  assert('m == 64);
+  assert(sizeof(xlen) == 64);
+
+  let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, vreg_name("v0"));
+  let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
+  let rs1_val				  = X(rs1);
+  let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
+  result      : vector('n, dec, bits('m)) = undefined;
+  mask        : vector('n, dec, bool)     = undefined;
+
+  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+
+  foreach (i from unsigned(vstart) to (unsigned(vl) - 1)) {
+    assert(0 <= i & i < 'n);
+    if mask[i] then {
+      let op1     : bits(64) = vs2_val[i];
+      let op2     : bits(64) = rs1_val;
+      let product : bits(64) = clmul(op1, op2);
+      result[i] = ~(op1) & op2;
+    };
+  };
+
+  write_single_vreg(num_elem, 'm, vd, result);
+  vstart = EXTZ(0b0);
+  RETIRE_SUCCESS
+}