diff --git a/model/riscv_insts_zvkb.sail b/model/riscv_insts_zvkb.sail
index deed76b19..5aed0b167 100644
--- a/model/riscv_insts_zvkb.sail
+++ b/model/riscv_insts_zvkb.sail
@@ -17,6 +17,15 @@ function clmul(x, y) = {
     result
 }
 
+val	 clmulh : forall 'm, 'm >= 0. (bits('m), bits('m)) -> bits('m)
+function clmulh(x, y) = {
+  result : bits('m) = zeros();
+  foreach (i from 0 to ('m - 1)) {
+    if y[i] == 0x1[1] then result = result ^ (x >> ('m - i));
+  };
+  result
+}
+
 /* VROL.VV */
 
 union clause ast = RISCV_VROL_VV : (bits(1), regidx, regidx, regidx)
@@ -466,7 +475,7 @@ mapping clause encdec = RISCV_VCLMUL_VX(vm, rs1, vs2, vd) if (haveRVV() & haveZv
  <-> 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)
+ <-> "vclmul.vx" ^ spc() ^ vreg_name(vd)
 		 ^ sep() ^ vreg_name(vs2)
 		 ^ sep() ^ reg_name(rs1)
 		 ^ maybe_vmask(vm)
@@ -505,3 +514,100 @@ function clause execute (RISCV_VCLMUL_VX(vm, rs1, vs2, vd)) = {
   vstart = EXTZ(0b0);
   RETIRE_SUCCESS
 }
+
+
+/* VCLMULH.VV */
+
+union clause ast = RISCV_VCLMULH_VV : (bits(1), regidx, regidx, regidx)
+
+mapping clause encdec = RISCV_VCLMULH_VV(vm, vs1, vs2, vd) if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+ <-> 0b001101 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111    if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+
+mapping clause assembly = RISCV_VCLMULH_VV(vm, vs1, vs2, vd)
+ <-> "vclmulh.vv" ^ spc() ^ vreg_name(vd)
+                  ^ sep() ^ vreg_name(vs2)
+                  ^ sep() ^ vreg_name(vs1)
+                  ^ maybe_vmask(vm)
+
+function clause execute (RISCV_VCLMULH_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) = clmulh(op1, op2);
+      result[i] = ~(op1) & op2;
+    };
+  };
+
+  write_single_vreg(num_elem, 'm, vd, result);
+  vstart = EXTZ(0b0);
+  RETIRE_SUCCESS
+}
+
+/* VCLMULH.VX */
+
+union clause ast = RISCV_VCLMULH_VX : (bits(1), regidx, regidx, regidx)
+
+mapping clause encdec = RISCV_VCLMULH_VX(vm, rs1, vs2, vd) if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+ <-> 0b001101 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111    if (haveRVV() & haveZvkb() & sizeof(xlen) == 64)
+
+mapping clause assembly = RISCV_VCLMULH_VX(vm, rs1, vs2, vd)
+ <-> "vclmulh.vx" ^ spc() ^ vreg_name(vd)
+                  ^ sep() ^ vreg_name(vs2)
+                  ^ sep() ^ reg_name(rs1)
+                  ^ maybe_vmask(vm)
+
+function clause execute (RISCV_VCLMULH_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) = clmulh(op1, op2);
+      result[i] = ~(op1) & op2;
+    };
+  };
+
+  write_single_vreg(num_elem, 'm, vd, result);
+  vstart = EXTZ(0b0);
+  RETIRE_SUCCESS
+}