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

8 files changed, 196 insertions, 27 deletions

diff --git a/Makefile b/Makefile
index 017cb13..8871ec7 100644
--- a/Makefile
+++ b/Makefile
@@ -33,6 +33,9 @@ SAIL_DEFAULT_INST += riscv_insts_zfh.sail
 SAIL_DEFAULT_INST += riscv_insts_zkn.sail
 SAIL_DEFAULT_INST += riscv_insts_zks.sail
 
+SAIL_DEFAULT_INST += riscv_insts_zbkb.sail
+SAIL_DEFAULT_INST += riscv_insts_zbkx.sail
+
 SAIL_SEQ_INST  = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
 SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail
 
diff --git a/model/prelude.sail b/model/prelude.sail
index 21c6793..6e6718b 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -270,6 +270,15 @@ function rotatel (v, n) =
 overload operator >>> = {rotate_bits_right, rotater}
 overload operator <<< = {rotate_bits_left, rotatel}
 
+function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
+  ys : bits(8) = zeros();
+  foreach (i from 0 to 7)
+    ys[i] = xs[7-i];
+  ys
+}
+
+overload reverse = {reverse_bits_in_byte}
+
 /* helpers for mappings */
 
 val spc : unit <-> string
diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail
index e3d2603..7b9fa89 100644
--- a/model/riscv_insts_zbb.sail
+++ b/model/riscv_insts_zbb.sail
@@ -1,8 +1,8 @@
 /* ****************************************************************** */
 union clause ast = RISCV_RORIW : (bits(5), regidx, regidx)
 
-mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+  <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_RORIW(shamt, rs1, rd)
   <-> "roriw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt)
@@ -17,8 +17,8 @@ function clause execute (RISCV_RORIW(shamt, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_RORI : (bits(6), regidx, regidx)
 
-mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if haveZbb() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
 
 mapping clause assembly = RISCV_RORI(shamt, rs1, rd)
   <-> "rori" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt)
@@ -35,11 +35,11 @@ function clause execute (RISCV_RORI(shamt, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = ZBB_RTYPEW : (regidx, regidx, regidx, bropw_zbb)
 
-mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
 
-mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
 
 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = {
   RISCV_ROLW <-> "rolw",
@@ -63,14 +63,14 @@ function clause execute (ZBB_RTYPEW(rs2, rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = ZBB_RTYPE : (regidx, regidx, regidx, brop_zbb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb()
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb() | haveZbkb()
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb()
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | haveZbkb()
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb()
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | haveZbkb()
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
 
 mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if haveZbb()
   <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb()
@@ -84,11 +84,11 @@ mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if haveZbb()
 mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MINU) if haveZbb()
   <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb()
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb()
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | haveZbkb()
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb()
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | haveZbkb()
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
 
 mapping zbb_rtype_mnemonic : brop_zbb <-> string = {
   RISCV_ANDN <-> "andn",
@@ -165,11 +165,11 @@ function clause execute (ZBB_EXTOP(rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_REV8 : (regidx, regidx)     
 
-mapping clause encdec = RISCV_REV8(rs1, rd) if haveZbb() & sizeof(xlen) == 32
-  <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb() & sizeof(xlen) == 32
+mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32
+  <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32
 
-mapping clause encdec = RISCV_REV8(rs1, rd) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+  <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_REV8(rs1, rd)
   <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail
index 8f69d88..ac74b50 100644
--- a/model/riscv_insts_zbc.sail
+++ b/model/riscv_insts_zbc.sail
@@ -1,8 +1,8 @@
 /* ****************************************************************** */
 union clause ast = RISCV_CLMUL : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_CLMUL(rs2, rs1, rd) if haveZbc()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbc()
+mapping clause encdec = RISCV_CLMUL(rs2, rs1, rd) if haveZbc() | haveZbkc()
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbc() | haveZbkc()
 
 mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd)
   <-> "clmul" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
@@ -20,8 +20,8 @@ function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CLMULH : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_CLMULH(rs2, rs1, rd) if haveZbc()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011 if haveZbc()
+mapping clause encdec = RISCV_CLMULH(rs2, rs1, rd) if haveZbc() | haveZbkc()
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011 if haveZbc() | haveZbkc()
 
 mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd)
   <-> "clmulh" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail
new file mode 100644
index 0000000..d8a6592
--- /dev/null
+++ b/model/riscv_insts_zbkb.sail
@@ -0,0 +1,105 @@
+/* ****************************************************************** */
+union clause ast = ZBKB_RTYPE : (regidx, regidx, regidx, brop_zbkb)
+
+mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACK) if haveZbkb()
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbkb()
+
+mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACKH) if haveZbkb()
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbkb()
+
+mapping zbkb_rtype_mnemonic : brop_zbkb <-> string = {
+  RISCV_PACK  <-> "pack",
+  RISCV_PACKH <-> "packh"
+}
+
+mapping clause assembly = ZBKB_RTYPE(rs2, rs1, rd, op)
+  <-> zbkb_rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+function clause execute (ZBKB_RTYPE(rs2, rs1, rd, op)) = {
+  let rs1_val = X(rs1);
+  let rs2_val = X(rs2);
+  let result : xlenbits = match op {
+    RISCV_PACK  => rs2_val[(sizeof(xlen_bytes)*4 - 1)..0] @ rs1_val[(sizeof(xlen_bytes)*4 - 1)..0],
+    RISCV_PACKH => EXTZ(rs2_val[7..0] @ rs1_val[7..0])
+  };
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
+
+/* ****************************************************************** */
+union clause ast = ZBKB_PACKW : (regidx, regidx, regidx)
+
+mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if haveZbkb() & sizeof(xlen) == 64
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZbkb() & sizeof(xlen) == 64
+
+mapping clause assembly = ZBKB_PACKW(rs2, rs1, rd)
+  <-> "packw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+function clause execute (ZBKB_PACKW(rs2, rs1, rd)) = {
+  assert(sizeof(xlen) == 64);
+  let rs1_val = X(rs1);
+  let rs2_val = X(rs2);
+  let result : bits(32) = rs2_val[15..0] @ rs1_val[15..0];
+  X(rd) = EXTZ(result);
+  RETIRE_SUCCESS
+}
+
+/* ****************************************************************** */
+union clause ast = RISCV_ZIP : (regidx, regidx)
+
+mapping clause encdec = RISCV_ZIP(rs1, rd) if haveZbkb() & sizeof(xlen) == 32
+  <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbkb() & sizeof(xlen) == 32
+
+mapping clause assembly = RISCV_ZIP(rs1, rd)
+  <-> "zip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
+
+function clause execute (RISCV_ZIP(rs1, rd)) = {
+  assert(sizeof(xlen) == 32);
+  let rs1_val = X(rs1);
+  result : xlenbits = zeros();
+  foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
+    result[i*2] = rs1_val[i];
+    result[i*2 + 1] = rs1_val[i + sizeof(xlen_bytes)*4];
+  };
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
+
+/* ****************************************************************** */
+union clause ast = RISCV_UNZIP : (regidx, regidx)
+
+mapping clause encdec = RISCV_UNZIP(rs1, rd) if haveZbkb() & sizeof(xlen) == 32
+  <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbkb() & sizeof(xlen) == 32
+
+mapping clause assembly = RISCV_UNZIP(rs1, rd)
+  <-> "unzip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
+
+function clause execute (RISCV_UNZIP(rs1, rd)) = {
+  assert(sizeof(xlen) == 32);
+  let rs1_val = X(rs1);
+  result : xlenbits = zeros();
+  foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
+    result[i] = rs1_val[i*2];
+    result[i + sizeof(xlen_bytes)*4] = rs1_val[i*2 + 1];
+  };
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
+
+/* ****************************************************************** */
+union clause ast = RISCV_BREV8 : (regidx, regidx)
+
+mapping clause encdec = RISCV_BREV8(rs1, rd) if haveZbkb()
+  <-> 0b011010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbkb()
+
+mapping clause assembly = RISCV_BREV8(rs1, rd)
+  <-> "brev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
+
+function clause execute (RISCV_BREV8(rs1, rd)) = {
+  let rs1_val = X(rs1);
+  result : xlenbits = zeros();
+  foreach (i from 0 to (sizeof(xlen) - 8) by 8)
+    result[i+7..i] = reverse(rs1_val[i+7..i]);
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
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
+}
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 916897d..d1f643a 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -189,7 +189,12 @@ function haveZbc()  -> bool = true
 function haveZbs()  -> bool = true
 
 /* Zfh (half-precision) extension */
-function haveZfh()    -> bool = true
+function haveZfh()  -> bool = true
+
+/* Scalar Cryptography extensions support. */
+function haveZbkb() -> bool = true
+function haveZbkc() -> bool = true
+function haveZbkx() -> bool = true
 
 /* Cryptography extension support. Note these will need updating once */
 /* Sail can be dynamically configured with different extension support */
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 08dce73..3e24698 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -396,6 +396,8 @@ enum brop_zbb = {RISCV_ANDN, RISCV_ORN, RISCV_XNOR, RISCV_MAX,
                  RISCV_MAXU, RISCV_MIN, RISCV_MINU, RISCV_ROL,
                  RISCV_ROR}
 
+enum brop_zbkb = {RISCV_PACK, RISCV_PACKH}
+
 enum brop_zbs = {RISCV_BCLR, RISCV_BEXT, RISCV_BINV, RISCV_BSET}
 
 enum bropw_zba = {RISCV_ADDUW, RISCV_SH1ADDUW, RISCV_SH2ADDUW,