diff --git a/README.md b/README.md index 767ec0270..31a50d2f2 100644 --- a/README.md +++ b/README.md @@ -187,6 +187,7 @@ For booting operating system images, see the information under the The following unratified extensions are supported and can be enabled using the `--enable-experimental-extensions` flag: - Zibi extension for conditional branches with immediate operands, v0.6 +- 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).** diff --git a/config/config.json.in b/config/config.json.in index e56823409..741da9cd4 100644 --- a/config/config.json.in +++ b/config/config.json.in @@ -415,6 +415,9 @@ "Zvkt": { "supported": true }, + "Zvzip": { + "supported": true + }, "Sscofpmf": { "supported": true }, diff --git a/doc/ChangeLog.md b/doc/ChangeLog.md index e1a34cca2..f2f55986a 100644 --- a/doc/ChangeLog.md +++ b/doc/ChangeLog.md @@ -17,6 +17,7 @@ - Smstateen, Sstateen - Ssqosid - Zibi + - Zvzip - The model now requires the Sail 0.20.1 compiler version. diff --git a/model/core/extensions.sail b/model/core/extensions.sail index 255310c65..274731c05 100644 --- a/model/core/extensions.sail +++ b/model/core/extensions.sail @@ -418,6 +418,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" @@ -561,6 +566,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 @@ -703,6 +709,9 @@ let extensions_ordered_for_isa_string = [ Ext_Zvl512b, Ext_Zvl1024b, + // Zvzip + Ext_Zvzip, + // Supervisor extensions, ordered alphabetically. Ext_Sscofpmf, Ext_Ssstateen, diff --git a/model/extensions/V/vext_utils_insts.sail b/model/extensions/V/vext_utils_insts.sail index 8794a9c02..7fdbae91a 100644 --- a/model/extensions/V/vext_utils_insts.sail +++ b/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. diff --git a/model/extensions/Zvzip/zvzip_insts.sail b/model/extensions/Zvzip/zvzip_insts.sail new file mode 100644 index 000000000..174b90c93 --- /dev/null +++ b/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 +} diff --git a/model/postlude/validate_config.sail b/model/postlude/validate_config.sail index de1830f40..4123da67e 100644 --- a/model/postlude/validate_config.sail +++ b/model/postlude/validate_config.sail @@ -174,6 +174,10 @@ private function check_vext_config() -> bool = { valid = false; print_endline("Zvkt is enabled but Zve32x is disabled: Zvkt requires Zve32x."); }; + if hartSupports(Ext_Zvzip) & not(hartSupports(Ext_Zve32x)) then { + valid = false; + print_endline("Zvzip is enabled but Zve32x is disabled: Zvzip requires Zve32x."); + }; valid; } diff --git a/model/riscv.sail_project b/model/riscv.sail_project index 73eb3a467..0c90304d6 100644 --- a/model/riscv.sail_project +++ b/model/riscv.sail_project @@ -500,6 +500,11 @@ extensions { } } + Zvzip { + requires core, sys, I, V + files extensions/Zvzip/zvzip_insts.sail + } + rmem { requires core, sys files