Add Unratified Zvzip extension instructions

README.md

@@ -184,9 +184,9 @@ For booting operating system images, see the information under the
 - Physical Memory Protection (PMP)
 - Static memory regions with some static PMAs (Physical Memory Attributes)
 
-<!-- Uncomment the following section when unratified extensions are added
 The following unratified extensions are supported and can be enabled using the `--enable-experimental-extensions` flag:
--  -->
+
+- Zvzip extension for Reordering Structured Data, v0.1
 
 **For a list of unsupported extensions and features, see the [Extension Roadmap](https://github.com/riscv/sail-riscv/wiki/Extension-Roadmap).**
 

config/config.json.in

@@ -400,6 +400,9 @@
     "Zvkt": {
       "supported": true
     },
+    "Zvzip": {
+      "supported": true
+    },
     "Sscofpmf": {
       "supported": true
     },

doc/ChangeLog.md

@@ -16,6 +16,7 @@
   - Ssu64xl
   - Smstateen, Sstateen
   - Ssqosid
+  - Zvzip
 
 - The model now requires the Sail 0.20.1 compiler version.
 

model/core/extensions.sail

@@ -415,6 +415,11 @@ mapping clause extensionName = Ext_Zvksg <-> "zvksg"
 function clause hartSupports(Ext_Zvksg) = hartSupports(Ext_Zvks) & hartSupports(Ext_Zvkg)
 function clause currentlyEnabled(Ext_Zvksg) = hartSupports(Ext_Zvksg)
 
+// Zvzip Extension for Reordering Structured Data
+enum clause extension = Ext_Zvzip
+mapping clause extensionName = Ext_Zvzip <-> "zvzip"
+function clause hartSupports(Ext_Zvzip) = sys_enable_experimental_extensions() & config extensions.Zvzip.supported
+
 // Count Overflow and Mode-Based Filtering
 enum clause extension = Ext_Sscofpmf
 mapping clause extensionName = Ext_Sscofpmf <-> "sscofpmf"
@@ -558,6 +563,7 @@ function currentlyEnabled_measure(ext : extension) -> int =
     Ext_Zvfbfmin => 3, // > Zve32f
     Ext_Zvkb => 3, // > Zvbb
     Ext_Zvknhb => 3, // > Zve64x
+    Ext_Zvzip => 3, // > Zve32x
 
     Ext_H => 4, // > virtual_mem_supported
     Ext_Zve64d => 4, // > Zve64f
@@ -699,6 +705,9 @@ let extensions_ordered_for_isa_string = [
   Ext_Zvl512b,
   Ext_Zvl1024b,
 
+  // Zvzip
+  Ext_Zvzip,
+
   // Supervisor extensions, ordered alphabetically.
   Ext_Sscofpmf,
   Ext_Ssstateen,

model/extensions/V/vext_utils_insts.sail

@@ -265,20 +265,13 @@ function get_start_element() -> result(nat, unit) = {
 // Get the ending element index from csr vl
 function get_end_element() -> int = unsigned(vl) - 1
 
-// Mask handling; creates a pre-masked result vector for vstart, vl, vta/vma, and vm
-// vm should be baked into vm_val from doing read_vmask
-// tail masking when lmul < 1 is handled in write_vreg
-// Returns two vectors:
-//   vector1 is the result vector with values applied to masked elements
-//   vector2 is a "mask" vector that is true for an element if the corresponding element
-//     in the result vector should be updated by the calling instruction
-val init_masked_result : forall 'n 'm 'p, 'n >= 0 . (int('n), int('m), int('p), vector('n, bits('m)), bits('n)) -> result((vector('n, bits('m)), bits('n)), unit)
-function init_masked_result(num_elem, _EEW, LMUL_pow, vd_val, vm_val) = {
+val init_masked_result_evl : forall 'n 'm 'e 'p, 'n >= 0 . (int('n), int('m), int('e), int('p), vector('n, bits('m)), bits('n)) -> result((vector('n, bits('m)), bits('n)), unit)
+function init_masked_result_evl(num_elem, _EEW, EVL, LMUL_pow, vd_val, vm_val) = {
   let start_element : nat = match get_start_element() {
     Ok(v)   => v,
     Err(()) => return Err(())
   };
-  let end_element   = get_end_element();
+  let end_element   = EVL - 1;
   let tail_ag : agtype = get_vtype_vta();
   let mask_ag : agtype = get_vtype_vma();
   var mask : bits('n) = undefined;
@@ -323,6 +316,18 @@ function init_masked_result(num_elem, _EEW, LMUL_pow, vd_val, vm_val) = {
   Ok((result, mask))
 }
 
+// Mask handling; creates a pre-masked result vector for vstart, vl, vta/vma, and vm
+// vm should be baked into vm_val from doing read_vmask
+// tail masking when lmul < 1 is handled in write_vreg
+// Returns two vectors:
+//   vector1 is the result vector with values applied to masked elements
+//   vector2 is a "mask" vector that is true for an element if the corresponding element
+//     in the result vector should be updated by the calling instruction
+val init_masked_result : forall 'n 'm 'p, 'n >= 0 . (int('n), int('m), int('p), vector('n, bits('m)), bits('n)) -> result((vector('n, bits('m)), bits('n)), unit)
+function init_masked_result(num_elem, _EEW, LMUL_pow, vd_val, vm_val) = {
+  init_masked_result_evl(num_elem, _EEW, unsigned(vl), LMUL_pow, vd_val, vm_val)
+}
+
 // For instructions like vector reduction and vector store,
 // masks on prestart, inactive and tail elements only affect the validation of source register elements
 // (vs3 for store and vs2 for reduction). There's no destination register to be masked.

model/extensions/Zvzip/zvzip_insts.sail

@@ -0,0 +1,254 @@
+// =======================================================================================
+// 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 currentlyEnabled(Ext_Zvzip) = hartSupports(Ext_Zvzip) & currentlyEnabled(Ext_Zve32x)
+
+union clause instruction = VZIP_VV : (bits(1), vregidx, vregidx, vregidx)
+
+$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
+mapping clause encdec = VZIP_VV(vm, vs1, vs2, vd)
+  <-> 0b111110 @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b010 @ encdec_vreg(vd) @ 0b1010111
+  when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
+
+mapping clause assembly = VZIP_VV(vm, vs1, vs2, vd)
+  <-> "vzip.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm)
+
+function clause execute VZIP_VV(vm, vs1, vs2, vd) = {
+  let SEW          = get_sew();
+  let LMUL_pow_src = get_lmul_pow();
+  let num_src_elem = get_num_elem(LMUL_pow_src, SEW);
+
+  assert(LMUL_pow_src <= 2);
+
+  let evl          = (unsigned(vl) * 2);
+  let LMUL_pow_dst = LMUL_pow_src + 1;
+  let num_dst_elem = get_num_elem(LMUL_pow_dst, SEW);
+
+  assert(num_dst_elem == 2 * num_src_elem);
+
+  if ((LMUL_pow_src == 3) |
+      not(valid_reg_overlap(vs2, vd, LMUL_pow_src, LMUL_pow_dst)) |
+      not(valid_reg_overlap(vs1, vd, LMUL_pow_src, LMUL_pow_dst)))
+  then return Illegal_Instruction();
+
+  let 'nd = num_dst_elem;
+  let 'ns = num_src_elem;
+  let 'm  = SEW;
+  let vm_val  : bits('nd)             = read_vmask(num_dst_elem, vm, zvreg);
+  let vs1_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs1);
+  let vs2_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs2);
+  let vd_val  : vector('nd, bits('m)) = read_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd);
+
+  let (initial_result, mask) : (vector('nd, bits('m)), bits('nd)) = match init_masked_result_evl(num_dst_elem, SEW, evl, LMUL_pow_dst, vd_val, vm_val) {
+      Ok(v)   => v,
+      Err(()) => return Illegal_Instruction()
+    };
+  var result = initial_result;
+
+  foreach (i from 0 to (num_dst_elem - 1)) {
+    let j = i / 2;
+
+    assert(j < num_src_elem);
+
+    if mask[i] == bitone then
+      result[i] = if (i % 2 == 0) then vs2_val[j] else vs1_val[j];
+  };
+  write_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd, result);
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}
+
+union clause instruction = VUNZIPE_V : (bits(1), vregidx, vregidx)
+
+$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
+mapping clause encdec = VUNZIPE_V(vm, vs2, vd)
+  <-> 0b010010 @ vm @ encdec_vreg(vs2) @ 0b01011 @ 0b010 @ encdec_vreg(vd) @ 0b1010111
+  when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
+
+mapping clause assembly = VUNZIPE_V(vm, vs2, vd)
+  <-> "vunzipe.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)
+
+function clause execute VUNZIPE_V(vm, vs2, vd) = {
+  let SEW          = get_sew();
+  let LMUL_pow_dst = get_lmul_pow();
+  let num_dst_elem = get_num_elem(LMUL_pow_dst, SEW);
+  let LMUL_pow_src = LMUL_pow_dst + 1;
+
+  assert(LMUL_pow_src <= 3);
+
+  let num_src_elem = get_num_elem(LMUL_pow_src, SEW);
+
+  assert(num_src_elem == 2 * num_dst_elem);
+
+  if ((LMUL_pow_dst == 3) |
+      not(valid_reg_overlap(vs2, vd, LMUL_pow_src, LMUL_pow_dst)))
+  then return Illegal_Instruction();
+
+  let 'nd = num_dst_elem;
+  let 'ns = num_src_elem;
+  let 'm  = SEW;
+  let vm_val  : bits('nd)             = read_vmask(num_dst_elem, vm, zvreg);
+  let vs2_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs2);
+  let vd_val  : vector('nd, bits('m)) = read_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd);
+
+  let (initial_result, mask) : (vector('nd, bits('m)), bits('nd)) = match init_masked_result(num_dst_elem, SEW, LMUL_pow_dst, vd_val, vm_val) {
+      Ok(v)   => v,
+      Err(()) => return Illegal_Instruction()
+    };
+  var result = initial_result;
+
+  foreach (i from 0 to (num_dst_elem - 1)) {
+    let j = 2 * i;
+
+    assert(j < num_src_elem);
+
+    if mask[i] == bitone then
+      result[i] = vs2_val[j];
+  };
+  write_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd, result);
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}
+
+union clause instruction = VUNZIPO_V : (bits(1), vregidx, vregidx)
+
+$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
+mapping clause encdec = VUNZIPO_V(vm, vs2, vd)
+  <-> 0b010010 @ vm @ encdec_vreg(vs2) @ 0b01111 @ 0b010 @ encdec_vreg(vd) @ 0b1010111
+  when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
+
+mapping clause assembly = VUNZIPO_V(vm, vs2, vd)
+  <-> "vunzipo.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)
+
+function clause execute VUNZIPO_V(vm, vs2, vd) = {
+  let SEW          = get_sew();
+  let LMUL_pow_dst = get_lmul_pow();
+  let num_dst_elem = get_num_elem(LMUL_pow_dst, SEW);
+  let LMUL_pow_src = LMUL_pow_dst + 1;
+
+  assert(LMUL_pow_src <= 3);
+
+  let num_src_elem = get_num_elem(LMUL_pow_src, SEW);
+
+  assert(num_src_elem == 2 * num_dst_elem);
+
+  if ((LMUL_pow_dst == 3) |
+      not(valid_reg_overlap(vs2, vd, LMUL_pow_src, LMUL_pow_dst)))
+  then return Illegal_Instruction();
+
+  let 'nd = num_dst_elem;
+  let 'ns = num_src_elem;
+  let 'm  = SEW;
+  let vm_val  : bits('nd)             = read_vmask(num_dst_elem, vm, zvreg);
+  let vs2_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs2);
+  let vd_val  : vector('nd, bits('m)) = read_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd);
+
+  let (initial_result, mask) : (vector('nd, bits('m)), bits('nd)) = match init_masked_result(num_dst_elem, SEW, LMUL_pow_dst, vd_val, vm_val) {
+      Ok(v)   => v,
+      Err(()) => return Illegal_Instruction()
+    };
+  var result = initial_result;
+
+  foreach (i from 0 to (num_dst_elem - 1)) {
+    let j = (2 * i) + 1;
+
+    assert(j < num_src_elem);
+
+    if mask[i] == bitone then
+      result[i] = vs2_val[j];
+  };
+  write_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd, result);
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}
+
+union clause instruction = VPAIRE_VV : (bits(1), vregidx, vregidx, vregidx)
+
+$[wavedrom "_ _ _ _ OPIVV _ OP-V"]
+mapping clause encdec = VPAIRE_VV(vm, vs1, vs2, vd)
+  <-> 0b001111 @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b000 @ encdec_vreg(vd) @ 0b1010111
+  when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
+
+mapping clause assembly = VPAIRE_VV(vm, vs1, vs2, vd)
+  <-> "vpaire.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm)
+
+function clause execute VPAIRE_VV(vm, vs1, vs2, vd) = {
+  if (vs1 == vd | vs2 == vd) then return Illegal_Instruction();
+  if ((vm == 0b1) & (vd == zvreg)) then return Illegal_Instruction();
+  let SEW      = get_sew();
+  let LMUL_pow = get_lmul_pow();
+  let num_elem = get_num_elem(LMUL_pow, SEW);
+  let 'n       = num_elem;
+  let 'm       = SEW;
+  let vm_val  : bits('n)             = read_vmask(num_elem, vm, zvreg);
+  let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
+  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 (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) {
+      Ok(v)   => v,
+      Err(()) => return Illegal_Instruction()
+    };
+  var result = initial_result;
+
+  foreach (i from 0 to (num_elem - 1)) {
+    if mask[i] == bitone then
+      result[i] = if (i % 2 == 0) then vs2_val[i] else vs1_val[i - 1];
+  };
+  write_vreg(num_elem, SEW, LMUL_pow, vd, result);
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}
+
+union clause instruction = VPAIRO_VV : (bits(1), vregidx, vregidx, vregidx)
+
+$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
+mapping clause encdec = VPAIRO_VV(vm, vs1, vs2, vd)
+  <-> 0b001111 @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b010 @ encdec_vreg(vd) @ 0b1010111
+  when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
+
+mapping clause assembly = VPAIRO_VV(vm, vs1, vs2, vd)
+  <-> "vpairo.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm)
+
+function clause execute VPAIRO_VV(vm, vs1, vs2, vd) = {
+  if (vs1 == vd | vs2 == vd) then return Illegal_Instruction();
+  if ((vm == 0b1) & (vd == zvreg)) then return Illegal_Instruction();
+  let SEW_pow  = get_sew_pow();
+  let SEW      = get_sew();
+  let LMUL_pow = get_lmul_pow();
+  let num_elem = get_num_elem(LMUL_pow, SEW);
+  let 'n       = num_elem;
+  let 'm       = SEW;
+  let vm_val  : bits('n)             = read_vmask(num_elem, vm, zvreg);
+  let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
+  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 (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) {
+      Ok(v)   => v,
+      Err(()) => return Illegal_Instruction()
+    };
+  var result = initial_result;
+
+  assert(LMUL_pow + vlen_exp - SEW_pow >= 0);
+  let VLMAX = 2 ^ (LMUL_pow + vlen_exp - SEW_pow);
+  assert(VLMAX <= 'n);
+  foreach (i from 0 to (num_elem - 1)) {
+    if mask[i] == bitone then
+      result[i] =
+        if (i % 2 == 0) then {
+          let idx = i + 1;
+          if idx < VLMAX then vs2_val[idx] else zeros()
+        } else {
+          vs1_val[i]
+        };
+  };
+  write_vreg(num_elem, SEW, LMUL_pow, vd, result);
+  set_vstart(zeros());
+  RETIRE_SUCCESS
+}

model/riscv.sail_project

@@ -488,6 +488,11 @@ extensions {
     }
   }
 
+  Zvzip {
+    requires core, sys, I, V
+    files extensions/Zvzip/zvzip_insts.sail
+  }
+
   rmem {
     requires core, sys
     files