Add support for Zvkg extension

Add following instructions:

vghsh.vv
vgmul.vv

Co-authored-by: Charalampos Mitrodimas <[email protected]>

Author: nadime15

README.md

@@ -119,6 +119,7 @@ Supported RISC-V ISA features
 - Zvbb extension for vector basic bit-manipulation, v1.0
 - Zvbc extension for vector carryless multiplication, v1.0
 - Zvkb extension for vector cryptography bit-manipulation, v1.0
+- Zvkg extension for vector GCM/GMAC, v1.0
 - Machine, Supervisor, and User modes
 - Smcntrpmf extension for cycle and instret privilege mode filtering, v1.0
 - Sscofpmf extension for Count Overflow and Mode-Based Filtering, v1.0

model/CMakeLists.txt

@@ -80,6 +80,7 @@ foreach (xlen IN ITEMS 32 64)
                 "riscv_insts_zicboz.sail"
                 "riscv_insts_zvbb.sail"
                 "riscv_insts_zvbc.sail"
+                "riscv_insts_zvkg.sail"
                 # Zimop and Zcmop should be at the end so they can be overridden by earlier extensions
                 "riscv_insts_zimop.sail"
                 "riscv_insts_zcmop.sail"
@@ -172,6 +173,7 @@ foreach (xlen IN ITEMS 32 64)
                 ${sail_vm_srcs}
                 # Shared/common code for the cryptography extension.
                 "riscv_types_kext.sail"
+                "riscv_types_zvk.sail"
             )
 
             if (variant STREQUAL "rvfi")

model/arithmetic.sail

@@ -6,6 +6,15 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+/* Reverse bits in each byte */
+val brev8 : forall 'm, 'm >= 0 & mod('m, 8) == 0. (bits('m)) -> bits('m)
+function brev8(input) = {
+  var output : bits('m) = zeros();
+  foreach (i from 0 to ('m - 8) by 8)
+    output[i+7..i] = reverse(input[i+7..i]);
+  output
+}
+
 /* Carry-less multiply. */
 val carryless_mul : forall 'n, 'n > 0. (bits('n), bits('n)) -> bits(2 * 'n)
 function carryless_mul(a, b) = {

model/riscv_extensions.sail

@@ -113,6 +113,8 @@ enum clause extension = Ext_Zvbb
 enum clause extension = Ext_Zvkb
 // Vector Carryless Multiplication
 enum clause extension = Ext_Zvbc
+// Vector GCM/GMAC
+enum clause extension = Ext_Zvkg
 
 // Count Overflow and Mode-Based Filtering
 enum clause extension = Ext_Sscofpmf

model/riscv_insts_vext_utils.sail

@@ -172,6 +172,17 @@ function get_scalar(rs1, SEW) = {
   }
 }
 
+/* Extracts 4 consecutive vector elements starting from index 4*i */
+val get_velem_4 : forall 'n 'm 'p, 'n > 0 & 8 <= 'm <= 64  & 'p >= 0 & 4 * 'p + 3 < 'n. (vector('n, bits('m)), int('p)) -> bits(4 * 'm)
+function get_velem_4(v, i) = v[4 * i + 3] @ v[4 * i + 2] @ v[4 * i + 1] @ v[4 * i]
+
+/* Divide the input bitvector into 4 equal slices and store them in vd starting at position 4*i */
+val set_velem_4 : forall 'p 'n 'm, 8 <= 'n <= 64 & 'm > 0 & 'p >= 0. (vregidx, int('n), bits('m), int('p)) -> unit
+function set_velem_4(vd, SEW, input, i) = {
+  foreach(j from 0 to 3)
+    write_single_element(SEW, 4 * i + j, vd, slice(input, j * SEW, SEW));
+}
+
 /* Get the starting element index from csr vtype */
 val get_start_element : unit -> nat
 function get_start_element() = {

model/riscv_insts_zvkg.sail

@@ -0,0 +1,107 @@
+/*=======================================================================================*/
+/*  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_Zvkg) = extensionEnabled(Ext_V)
+
+union clause ast = VGHSH_VV : (vregidx, vregidx, vregidx)
+
+mapping clause encdec = VGHSH_VV(vs2, vs1, vd)
+  <-> 0b1011001 @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b010 @ encdec_vreg(vd) @ 0b1110111
+  when extensionEnabled(Ext_Zvkg) & get_sew() == 32 & zvk_check_encdec(128, 4)
+
+mapping clause assembly = VGHSH_VV(vs2, vs1, vd)
+  <-> "vghsh.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2)^ sep() ^ vreg_name(vs1)
+
+function clause execute (VGHSH_VV(vs2, vs1, vd)) = {
+  let SEW      = get_sew();
+  let LMUL_pow = get_lmul_pow();
+  let num_elem = get_num_elem(LMUL_pow, SEW);
+
+  assert(SEW == 32);
+
+  let 'n = num_elem;
+  let 'm = SEW;
+
+  let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
+  let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
+  let vd_val  : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
+
+  let eg_len   = (unsigned(vl) / 4);
+  let eg_start = (unsigned(vstart) / 4);
+
+  foreach (i from eg_start to (eg_len - 1)) {
+    assert(0 <= i & ((i * 4) + 3) < 'n);
+
+    let Y : bits(128) = get_velem_4(vd_val, i);
+    let X : bits(128) = get_velem_4(vs1_val, i);
+    var H : bits(128) = brev8(get_velem_4(vs2_val, i));
+
+    var Z : bits(128) = zeros();
+    let S : bits(128) = brev8(Y ^ X);
+
+    foreach (b from 0 to 127) {
+      if S[b] == bitone then Z = Z ^ H;
+
+      let reduce = H[127] == bitone;
+      H = H << 1;
+      if reduce then H = H[127..8] @ (H[7..0] ^ 0x87);
+    };
+
+    set_velem_4(vd, SEW, brev8(Z), i);
+  };
+
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}
+
+union clause ast = VGMUL_VV : (vregidx, vregidx)
+
+mapping clause encdec = VGMUL_VV(vs2, vd)
+  <-> 0b1010001 @ encdec_vreg(vs2) @ 0b10001 @ 0b010 @ encdec_vreg(vd) @ 0b1110111
+  when extensionEnabled(Ext_Zvkg) & get_sew() == 32 & zvk_check_encdec(128, 4)
+
+mapping clause assembly = VGMUL_VV(vs2, vd)
+  <-> "vgmul.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2)
+
+function clause execute (VGMUL_VV(vs2, vd)) = {
+  let SEW      = get_sew();
+  let LMUL_pow = get_lmul_pow();
+  let num_elem = get_num_elem(LMUL_pow, SEW);
+
+  assert(SEW == 32);
+
+  let 'n = num_elem;
+  let 'm = SEW;
+
+  let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
+  let vd_val  : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
+
+  let eg_len   = (unsigned(vl) / 4);
+  let eg_start = (unsigned(vstart) / 4);
+
+  foreach (i from eg_start to (eg_len - 1)) {
+    assert(0 <= i & ((i * 4) + 3) < 'n);
+
+    let Y : bits(128) = brev8(get_velem_4(vd_val, i));
+    var H : bits(128) = brev8(get_velem_4(vs2_val, i));
+    var Z : bits(128) = zeros();
+
+    foreach (b from 0 to 127) {
+      if Y[b] == bitone then Z = Z ^ H;
+
+      let reduce = H[127] == bitone;
+      H = H << 1;
+      if reduce then H = H[127..8] @ (H[7..0] ^ 0x87);
+    };
+
+    set_velem_4(vd, SEW, brev8(Z), i);
+  };
+
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}

model/riscv_types_zvk.sail

@@ -0,0 +1,9 @@
+/*=======================================================================================*/
+/*  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 zvk_check_encdec(EGW: int, EGS: {4}) -> bool = (unsigned(vl) % EGS == 0) & (unsigned(vstart) % EGS == 0) & (2 ^ get_lmul_pow() * VLEN) >= EGW