Skip to content

Commit c08efc7

Browse files
ved-rivosved-rivos
committed
Add Zvzip extension instructions
1 parent f0b6fb1 commit c08efc7

File tree

7 files changed

+288
-12
lines changed

7 files changed

+288
-12
lines changed

‎README.md‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -184,9 +184,8 @@ For booting operating system images, see the information under the
184184
- Physical Memory Protection (PMP)
185185
- Static memory regions with some static PMAs (Physical Memory Attributes)
186186

187-
<!-- Uncomment the following section when unratified extensions are added
188187
The following unratified extensions are supported and can be enabled using the `--enable-experimental-extensions` flag:
189-
- -->
188+
- Zvzip extension for Reordering Structured Data, v0.1
190189

191190
**For a list of unsupported extensions and features, see the [Extension Roadmap](https://github.com/riscv/sail-riscv/wiki/Extension-Roadmap).**
192191

‎config/config.json.in‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -400,6 +400,9 @@
400400
"Zvkt": {
401401
"supported": true
402402
},
403+
"Zvzip": {
404+
"supported": true
405+
},
403406
"Sscofpmf": {
404407
"supported": true
405408
},

‎doc/ChangeLog.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
- Ssu64xl
1717
- Smstateen, Sstateen
1818
- Ssqosid
19+
- Zvzip
1920

2021
- The model now requires the Sail 0.20.1 compiler version.
2122

‎model/core/extensions.sail‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -415,6 +415,11 @@ mapping clause extensionName = Ext_Zvksg <-> "zvksg"
415415
function clause hartSupports(Ext_Zvksg) = hartSupports(Ext_Zvks) & hartSupports(Ext_Zvkg)
416416
function clause currentlyEnabled(Ext_Zvksg) = hartSupports(Ext_Zvksg)
417417

418+
// Zvzip Extension for Reordering Structured Data
419+
enum clause extension = Ext_Zvzip
420+
mapping clause extensionName = Ext_Zvzip <-> "zvzip"
421+
function clause hartSupports(Ext_Zvzip) = sys_enable_experimental_extensions() & config extensions.Zvzip.supported
422+
418423
// Count Overflow and Mode-Based Filtering
419424
enum clause extension = Ext_Sscofpmf
420425
mapping clause extensionName = Ext_Sscofpmf <-> "sscofpmf"
@@ -558,6 +563,7 @@ function currentlyEnabled_measure(ext : extension) -> int =
558563
Ext_Zvfbfmin => 3, // > Zve32f
559564
Ext_Zvkb => 3, // > Zvbb
560565
Ext_Zvknhb => 3, // > Zve64x
566+
Ext_Zvzip => 3, // > Zve32x
561567

562568
Ext_H => 4, // > virtual_mem_supported
563569
Ext_Zve64d => 4, // > Zve64f
@@ -699,6 +705,9 @@ let extensions_ordered_for_isa_string = [
699705
Ext_Zvl512b,
700706
Ext_Zvl1024b,
701707

708+
// Zvzip
709+
Ext_Zvzip,
710+
702711
// Supervisor extensions, ordered alphabetically.
703712
Ext_Sscofpmf,
704713
Ext_Ssstateen,

‎model/extensions/V/vext_utils_insts.sail‎

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -265,20 +265,13 @@ function get_start_element() -> result(nat, unit) = {
265265
// Get the ending element index from csr vl
266266
function get_end_element() -> int = unsigned(vl) - 1
267267

268-
// Mask handling; creates a pre-masked result vector for vstart, vl, vta/vma, and vm
269-
// vm should be baked into vm_val from doing read_vmask
270-
// tail masking when lmul < 1 is handled in write_vreg
271-
// Returns two vectors:
272-
// vector1 is the result vector with values applied to masked elements
273-
// vector2 is a "mask" vector that is true for an element if the corresponding element
274-
// in the result vector should be updated by the calling instruction
275-
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)
276-
function init_masked_result(num_elem, _EEW, LMUL_pow, vd_val, vm_val) = {
268+
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)
269+
function init_masked_result_evl(num_elem, _EEW, EVL, LMUL_pow, vd_val, vm_val) = {
277270
let start_element : nat = match get_start_element() {
278271
Ok(v) => v,
279272
Err(()) => return Err(())
280273
};
281-
let end_element = get_end_element();
274+
let end_element = EVL - 1;
282275
let tail_ag : agtype = get_vtype_vta();
283276
let mask_ag : agtype = get_vtype_vma();
284277
var mask : bits('n) = undefined;
@@ -323,6 +316,18 @@ function init_masked_result(num_elem, _EEW, LMUL_pow, vd_val, vm_val) = {
323316
Ok((result, mask))
324317
}
325318

319+
// Mask handling; creates a pre-masked result vector for vstart, vl, vta/vma, and vm
320+
// vm should be baked into vm_val from doing read_vmask
321+
// tail masking when lmul < 1 is handled in write_vreg
322+
// Returns two vectors:
323+
// vector1 is the result vector with values applied to masked elements
324+
// vector2 is a "mask" vector that is true for an element if the corresponding element
325+
// in the result vector should be updated by the calling instruction
326+
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)
327+
function init_masked_result(num_elem, _EEW, LMUL_pow, vd_val, vm_val) = {
328+
init_masked_result_evl(num_elem, _EEW, unsigned(vl), LMUL_pow, vd_val, vm_val)
329+
}
330+
326331
// For instructions like vector reduction and vector store,
327332
// masks on prestart, inactive and tail elements only affect the validation of source register elements
328333
// (vs3 for store and vs2 for reduction). There's no destination register to be masked.

‎model/extensions/Zvzip/zvzip_insts.sail‎

Lines changed: 254 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,254 @@
1+
// =======================================================================================
2+
// This Sail RISC-V architecture model, comprising all files and
3+
// directories except where otherwise noted is subject the BSD
4+
// two-clause license in the LICENSE file.
5+
//
6+
// SPDX-License-Identifier: BSD-2-Clause
7+
// =======================================================================================
8+
9+
function clause currentlyEnabled(Ext_Zvzip) = hartSupports(Ext_Zvzip) & currentlyEnabled(Ext_Zve32x)
10+
11+
union clause instruction = VZIP_VV : (bits(1), vregidx, vregidx, vregidx)
12+
13+
$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
14+
mapping clause encdec = VZIP_VV(vm, vs1, vs2, vd)
15+
<-> 0b111110 @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b010 @ encdec_vreg(vd) @ 0b1010111
16+
when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
17+
18+
mapping clause assembly = VZIP_VV(vm, vs1, vs2, vd)
19+
<-> "vzip.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm)
20+
21+
function clause execute VZIP_VV(vm, vs1, vs2, vd) = {
22+
let SEW = get_sew();
23+
let LMUL_pow_src = get_lmul_pow();
24+
let num_src_elem = get_num_elem(LMUL_pow_src, SEW);
25+
26+
assert(LMUL_pow_src <= 2);
27+
28+
let evl = (unsigned(vl) * 2);
29+
let LMUL_pow_dst = LMUL_pow_src + 1;
30+
let num_dst_elem = get_num_elem(LMUL_pow_dst, SEW);
31+
32+
assert(num_dst_elem == 2 * num_src_elem);
33+
34+
if ((LMUL_pow_src == 3) |
35+
not(valid_reg_overlap(vs2, vd, LMUL_pow_src, LMUL_pow_dst)) |
36+
not(valid_reg_overlap(vs1, vd, LMUL_pow_src, LMUL_pow_dst)))
37+
then return Illegal_Instruction();
38+
39+
let 'nd = num_dst_elem;
40+
let 'ns = num_src_elem;
41+
let 'm = SEW;
42+
let vm_val : bits('nd) = read_vmask(num_dst_elem, vm, zvreg);
43+
let vs1_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs1);
44+
let vs2_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs2);
45+
let vd_val : vector('nd, bits('m)) = read_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd);
46+
47+
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) {
48+
Ok(v) => v,
49+
Err(()) => return Illegal_Instruction()
50+
};
51+
var result = initial_result;
52+
53+
foreach (i from 0 to (num_dst_elem - 1)) {
54+
let j = i / 2;
55+
56+
assert(j < num_src_elem);
57+
58+
if mask[i] == bitone then
59+
result[i] = if (i % 2 == 0) then vs2_val[j] else vs1_val[j];
60+
};
61+
write_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd, result);
62+
set_vstart(zeros());
63+
RETIRE_SUCCESS
64+
}
65+
66+
union clause instruction = VUNZIPE_V : (bits(1), vregidx, vregidx)
67+
68+
$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
69+
mapping clause encdec = VUNZIPE_V(vm, vs2, vd)
70+
<-> 0b010010 @ vm @ encdec_vreg(vs2) @ 0b01011 @ 0b010 @ encdec_vreg(vd) @ 0b1010111
71+
when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
72+
73+
mapping clause assembly = VUNZIPE_V(vm, vs2, vd)
74+
<-> "vunzipe.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)
75+
76+
function clause execute VUNZIPE_V(vm, vs2, vd) = {
77+
let SEW = get_sew();
78+
let LMUL_pow_dst = get_lmul_pow();
79+
let num_dst_elem = get_num_elem(LMUL_pow_dst, SEW);
80+
let LMUL_pow_src = LMUL_pow_dst + 1;
81+
82+
assert(LMUL_pow_src <= 3);
83+
84+
let num_src_elem = get_num_elem(LMUL_pow_src, SEW);
85+
86+
assert(num_src_elem == 2 * num_dst_elem);
87+
88+
if ((LMUL_pow_dst == 3) |
89+
not(valid_reg_overlap(vs2, vd, LMUL_pow_src, LMUL_pow_dst)))
90+
then return Illegal_Instruction();
91+
92+
let 'nd = num_dst_elem;
93+
let 'ns = num_src_elem;
94+
let 'm = SEW;
95+
let vm_val : bits('nd) = read_vmask(num_dst_elem, vm, zvreg);
96+
let vs2_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs2);
97+
let vd_val : vector('nd, bits('m)) = read_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd);
98+
99+
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) {
100+
Ok(v) => v,
101+
Err(()) => return Illegal_Instruction()
102+
};
103+
var result = initial_result;
104+
105+
foreach (i from 0 to (num_dst_elem - 1)) {
106+
let j = 2 * i;
107+
108+
assert(j < num_src_elem);
109+
110+
if mask[i] == bitone then
111+
result[i] = vs2_val[j];
112+
};
113+
write_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd, result);
114+
set_vstart(zeros());
115+
RETIRE_SUCCESS
116+
}
117+
118+
union clause instruction = VUNZIPO_V : (bits(1), vregidx, vregidx)
119+
120+
$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
121+
mapping clause encdec = VUNZIPO_V(vm, vs2, vd)
122+
<-> 0b010010 @ vm @ encdec_vreg(vs2) @ 0b01111 @ 0b010 @ encdec_vreg(vd) @ 0b1010111
123+
when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
124+
125+
mapping clause assembly = VUNZIPO_V(vm, vs2, vd)
126+
<-> "vunzipo.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)
127+
128+
function clause execute VUNZIPO_V(vm, vs2, vd) = {
129+
let SEW = get_sew();
130+
let LMUL_pow_dst = get_lmul_pow();
131+
let num_dst_elem = get_num_elem(LMUL_pow_dst, SEW);
132+
let LMUL_pow_src = LMUL_pow_dst + 1;
133+
134+
assert(LMUL_pow_src <= 3);
135+
136+
let num_src_elem = get_num_elem(LMUL_pow_src, SEW);
137+
138+
assert(num_src_elem == 2 * num_dst_elem);
139+
140+
if ((LMUL_pow_dst == 3) |
141+
not(valid_reg_overlap(vs2, vd, LMUL_pow_src, LMUL_pow_dst)))
142+
then return Illegal_Instruction();
143+
144+
let 'nd = num_dst_elem;
145+
let 'ns = num_src_elem;
146+
let 'm = SEW;
147+
let vm_val : bits('nd) = read_vmask(num_dst_elem, vm, zvreg);
148+
let vs2_val : vector('ns, bits('m)) = read_vreg(num_src_elem, SEW, LMUL_pow_src, vs2);
149+
let vd_val : vector('nd, bits('m)) = read_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd);
150+
151+
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) {
152+
Ok(v) => v,
153+
Err(()) => return Illegal_Instruction()
154+
};
155+
var result = initial_result;
156+
157+
foreach (i from 0 to (num_dst_elem - 1)) {
158+
let j = (2 * i) + 1;
159+
160+
assert(j < num_src_elem);
161+
162+
if mask[i] == bitone then
163+
result[i] = vs2_val[j];
164+
};
165+
write_vreg(num_dst_elem, SEW, LMUL_pow_dst, vd, result);
166+
set_vstart(zeros());
167+
RETIRE_SUCCESS
168+
}
169+
170+
union clause instruction = VPAIRE_VV : (bits(1), vregidx, vregidx, vregidx)
171+
172+
$[wavedrom "_ _ _ _ OPIVV _ OP-V"]
173+
mapping clause encdec = VPAIRE_VV(vm, vs1, vs2, vd)
174+
<-> 0b001111 @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b000 @ encdec_vreg(vd) @ 0b1010111
175+
when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
176+
177+
mapping clause assembly = VPAIRE_VV(vm, vs1, vs2, vd)
178+
<-> "vpaire.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm)
179+
180+
function clause execute VPAIRE_VV(vm, vs1, vs2, vd) = {
181+
if (vs1 == vd | vs2 == vd) then return Illegal_Instruction();
182+
if ((vm == 0b1) & (vd == Vregidx(0b00000))) then return Illegal_Instruction();
183+
let SEW = get_sew();
184+
let LMUL_pow = get_lmul_pow();
185+
let num_elem = get_num_elem(LMUL_pow, SEW);
186+
let 'n = num_elem;
187+
let 'm = SEW;
188+
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
189+
let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
190+
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
191+
let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
192+
193+
let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) {
194+
Ok(v) => v,
195+
Err(()) => return Illegal_Instruction()
196+
};
197+
var result = initial_result;
198+
199+
foreach (i from 0 to (num_elem - 1)) {
200+
if mask[i] == bitone then
201+
result[i] = if (i % 2 == 0) then vs2_val[i] else vs1_val[i - 1];
202+
};
203+
write_vreg(num_elem, SEW, LMUL_pow, vd, result);
204+
set_vstart(zeros());
205+
RETIRE_SUCCESS
206+
}
207+
208+
union clause instruction = VPAIRO_VV : (bits(1), vregidx, vregidx, vregidx)
209+
210+
$[wavedrom "_ _ _ _ OPMVV _ OP-V"]
211+
mapping clause encdec = VPAIRO_VV(vm, vs1, vs2, vd)
212+
<-> 0b001111 @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b010 @ encdec_vreg(vd) @ 0b1010111
213+
when currentlyEnabled(Ext_Zvzip) & (get_sew() <= 32 | (get_sew() == 64 & currentlyEnabled(Ext_Zve64x)))
214+
215+
mapping clause assembly = VPAIRO_VV(vm, vs1, vs2, vd)
216+
<-> "vpairo.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm)
217+
218+
function clause execute VPAIRO_VV(vm, vs1, vs2, vd) = {
219+
if (vs1 == vd | vs2 == vd) then return Illegal_Instruction();
220+
if ((vm == 0b1) & (vd == Vregidx(0b00000))) then return Illegal_Instruction();
221+
let SEW_pow = get_sew_pow();
222+
let SEW = get_sew();
223+
let LMUL_pow = get_lmul_pow();
224+
let num_elem = get_num_elem(LMUL_pow, SEW);
225+
let 'n = num_elem;
226+
let 'm = SEW;
227+
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
228+
let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
229+
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
230+
let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
231+
232+
let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) {
233+
Ok(v) => v,
234+
Err(()) => return Illegal_Instruction()
235+
};
236+
var result = initial_result;
237+
238+
assert(LMUL_pow + vlen_exp - SEW_pow >= 0);
239+
let VLMAX = 2 ^ (LMUL_pow + vlen_exp - SEW_pow);
240+
assert(VLMAX <= 'n);
241+
foreach (i from 0 to (num_elem - 1)) {
242+
if mask[i] == bitone then
243+
result[i] =
244+
if (i % 2 == 0) then {
245+
let idx = i + 1;
246+
if idx < VLMAX then vs2_val[idx] else zeros()
247+
} else {
248+
vs1_val[i]
249+
};
250+
};
251+
write_vreg(num_elem, SEW, LMUL_pow, vd, result);
252+
set_vstart(zeros());
253+
RETIRE_SUCCESS
254+
}

‎model/riscv.sail_project‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -487,6 +487,11 @@ extensions {
487487
}
488488
}
489489

490+
Zvzip {
491+
requires sys, I, V
492+
files extensions/Zvzip/zvzip_insts.sail
493+
}
494+
490495
rmem {
491496
requires core, sys
492497
files

0 commit comments

Comments
 (0)