Add support for Scalar Cryptography Zbkb, Zbkc and Zbkx Extensions (#135)

1 files changed, 45 insertions, 0 deletions

diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail
new file mode 100644
index 0000000..890facf
--- /dev/null
+++ b/model/riscv_insts_zbkx.sail
@@ -0,0 +1,45 @@
+/* ****************************************************************** */
+union clause ast = RISCV_XPERM8 : (regidx, regidx, regidx)
+
+mapping clause encdec = RISCV_XPERM8(rs2, rs1, rd) if haveZbkx()
+  <-> 0b0010100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbkx()
+
+mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd)
+  <-> "xperm8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = {
+  let rs1_val = X(rs1);
+  let rs2_val = X(rs2);
+  result : xlenbits = zeros();
+  foreach (i from 0 to (sizeof(xlen) - 8) by 8) {
+    let index = unsigned(rs2_val[i+7..i]);
+    result[i+7..i] = if 8*index < sizeof(xlen)
+                     then rs1_val[8*index+7..8*index]
+                     else zeros()
+  };
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
+
+/* ****************************************************************** */
+union clause ast = RISCV_XPERM4 : (regidx, regidx, regidx)
+
+mapping clause encdec = RISCV_XPERM4(rs2, rs1, rd) if haveZbkx()
+  <-> 0b0010100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZbkx()
+
+mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd)
+  <-> "xperm4" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+function clause execute (RISCV_XPERM4(rs2, rs1, rd)) = {
+  let rs1_val = X(rs1);
+  let rs2_val = X(rs2);
+  result : xlenbits = zeros();
+  foreach (i from 0 to (sizeof(xlen) - 4) by 4) {
+    let index = unsigned(rs2_val[i+3..i]);
+    result[i+3..i] = if 8*index < sizeof(xlen)
+                     then rs1_val[8*index+3..8*index]
+                     else zeros()
+  };
+  X(rd) = result;
+  RETIRE_SUCCESS
+}