Skip to content

Commit 1cb0831

Browse files
TimmmmTimmmm
committed
Remove explicit type annotations and redundant type variables in Vector code
This removes a load of the redundant type variables `let 'n = num_elem` in favour of using `'num_elem` directly (and similarly for `SEW`). I also removed a load of the explicit type annotations which are not needed.
1 parent a9ac9dc commit 1cb0831

9 files changed

+564
-864
lines changed

‎model/riscv_insts_vext_arith.sail

+256-355
Large diffs are not rendered by default.

‎model/riscv_insts_vext_fp.sail

+104-166
Large diffs are not rendered by default.

‎model/riscv_insts_vext_fp_red.sail

+10-19
Original file line numberDiff line numberDiff line change
@@ -37,16 +37,12 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
3737

3838
if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
3939

40-
let 'n = num_elem_vs;
41-
let 'd = num_elem_vd;
42-
let 'm = SEW;
40+
let vm_val = read_vmask(num_elem_vs, vm, zvreg);
41+
let vd_val = read_vreg(num_elem_vd, SEW, 0, vd);
42+
let vs2_val = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
43+
let mask = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
4344

44-
let vm_val : bits('n) = read_vmask(num_elem_vs, vm, zvreg);
45-
let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd);
46-
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
47-
let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
48-
49-
var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
45+
var sum = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
5046
foreach (i from 0 to (num_elem_vs - 1)) {
5147
if mask[i] == bitone then {
5248
sum = match funct6 {
@@ -79,17 +75,12 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow
7975

8076
if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
8177

82-
let 'n = num_elem_vs;
83-
let 'd = num_elem_vd;
84-
let 'm = SEW;
85-
let 'o = SEW_widen;
86-
87-
let vm_val : bits('n) = read_vmask(num_elem_vs, vm, zvreg);
88-
let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd);
89-
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
90-
let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
78+
let vm_val = read_vmask(num_elem_vs, vm, zvreg);
79+
let vd_val = read_vreg(num_elem_vd, SEW_widen, 0, vd);
80+
let vs2_val = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
81+
let mask = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
9182

92-
var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
83+
var sum = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
9384
foreach (i from 0 to (num_elem_vs - 1)) {
9485
if mask[i] == bitone then {
9586
/* currently ordered/unordered sum reductions do the same operations */

‎model/riscv_insts_vext_fp_vm.sail

+8-14
Original file line numberDiff line numberDiff line change
@@ -35,13 +35,10 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
3535
if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL };
3636
assert(SEW != 8);
3737

38-
let 'n = num_elem;
39-
let 'm = SEW;
40-
41-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
42-
let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
43-
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
44-
let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd);
38+
let vm_val = read_vmask(num_elem, vm, zvreg);
39+
let vs1_val = read_vreg(num_elem, SEW, LMUL_pow, vs1);
40+
let vs2_val = read_vreg(num_elem, SEW, LMUL_pow, vs2);
41+
let vd_val = read_vmask(num_elem, 0b0, vd);
4542

4643
let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
4744
var result = initial_result;
@@ -99,13 +96,10 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
9996
if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL };
10097
assert(SEW != 8);
10198

102-
let 'n = num_elem;
103-
let 'm = SEW;
104-
105-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
106-
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
107-
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
108-
let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd);
99+
let vm_val = read_vmask(num_elem, vm, zvreg);
100+
let rs1_val = get_scalar_fp(rs1, SEW);
101+
let vs2_val = read_vreg(num_elem, SEW, LMUL_pow, vs2);
102+
let vd_val = read_vmask(num_elem, 0b0, vd);
109103

110104
let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
111105
var result = initial_result;

‎model/riscv_insts_vext_mask.sail

+21-45
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,9 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
3636

3737
if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL };
3838

39-
let 'n = num_elem;
40-
let 'm = SEW;
41-
42-
let vs1_val : bits('n) = read_vmask(num_elem, 0b0, vs1);
43-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
44-
let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd);
39+
let vs1_val = read_vmask(num_elem, 0b0, vs1);
40+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
41+
let vd_val = read_vmask(num_elem, 0b0, vd);
4542

4643
let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val);
4744
var result = initial_result;
@@ -94,11 +91,8 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = {
9491

9592
if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL };
9693

97-
let 'n = num_elem;
98-
let 'm = SEW;
99-
100-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
101-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
94+
let vm_val = read_vmask(num_elem, vm, zvreg);
95+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
10296

10397
let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
10498

@@ -129,11 +123,8 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = {
129123

130124
if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL };
131125

132-
let 'n = num_elem;
133-
let 'm = SEW;
134-
135-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
136-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
126+
let vm_val = read_vmask(num_elem, vm, zvreg);
127+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
137128

138129
let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
139130

@@ -167,12 +158,9 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = {
167158
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
168159
then { handle_illegal(); return RETIRE_FAIL };
169160

170-
let 'n = num_elem;
171-
let 'm = SEW;
172-
173-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
174-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
175-
let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd);
161+
let vm_val = read_vmask(num_elem, vm, zvreg);
162+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
163+
let vd_val = read_vmask(num_elem, 0b0, vd);
176164

177165
let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
178166
var result = initial_result;
@@ -208,12 +196,9 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = {
208196
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
209197
then { handle_illegal(); return RETIRE_FAIL };
210198

211-
let 'n = num_elem;
212-
let 'm = SEW;
213-
214-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
215-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
216-
let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd);
199+
let vm_val = read_vmask(num_elem, vm, zvreg);
200+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
201+
let vd_val = read_vmask(num_elem, 0b0, vd);
217202

218203
let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
219204
var result = initial_result;
@@ -249,12 +234,9 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = {
249234
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
250235
then { handle_illegal(); return RETIRE_FAIL };
251236

252-
let 'n = num_elem;
253-
let 'm = SEW;
254-
255-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
256-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
257-
let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd);
237+
let vm_val = read_vmask(num_elem, vm, zvreg);
238+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
239+
let vd_val = read_vmask(num_elem, 0b0, vd);
258240

259241
let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
260242
var result = initial_result;
@@ -294,12 +276,9 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = {
294276
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
295277
then { handle_illegal(); return RETIRE_FAIL };
296278

297-
let 'n = num_elem;
298-
let 'm = SEW;
299-
300-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
301-
let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2);
302-
let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
279+
let vm_val = read_vmask(num_elem, vm, zvreg);
280+
let vs2_val = read_vmask(num_elem, 0b0, vs2);
281+
let vd_val = read_vreg(num_elem, SEW, LMUL_pow, vd);
303282

304283
let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
305284
var result = initial_result;
@@ -334,11 +313,8 @@ function clause execute(VID_V(vm, vd)) = {
334313

335314
if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL };
336315

337-
let 'n = num_elem;
338-
let 'm = SEW;
339-
340-
let vm_val : bits('n) = read_vmask(num_elem, vm, zvreg);
341-
let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
316+
let vm_val = read_vmask(num_elem, vm, zvreg);
317+
let vd_val = read_vreg(num_elem, SEW, LMUL_pow, vd);
342318

343319
let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
344320
var result = initial_result;

‎model/riscv_insts_vext_red.sail

+12-21
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ mapping clause encdec = RIVVTYPE(funct6, vm, vs2, vs1, vd)
2626
function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = {
2727
let SEW = get_sew();
2828
let LMUL_pow = get_lmul_pow();
29-
let SEW_widen = SEW * 2;
29+
let 'SEW_widen = SEW * 2;
3030
let LMUL_pow_widen = LMUL_pow + 1;
3131
let num_elem_vs = get_num_elem(LMUL_pow, SEW);
3232
let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */
@@ -35,20 +35,15 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = {
3535

3636
if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
3737

38-
let 'n = num_elem_vs;
39-
let 'd = num_elem_vd;
40-
let 'm = SEW;
41-
let 'o = SEW_widen;
38+
let vm_val = read_vmask(num_elem_vs, vm, zvreg);
39+
let vd_val = read_vreg(num_elem_vd, SEW_widen, 0, vd);
40+
let vs2_val = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
41+
let mask = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
4242

43-
let vm_val : bits('n) = read_vmask(num_elem_vs, vm, zvreg);
44-
let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd);
45-
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
46-
let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
47-
48-
var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
43+
var sum = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
4944
foreach (i from 0 to (num_elem_vs - 1)) {
5045
if mask[i] == bitone then {
51-
let elem : bits('o) = match funct6 {
46+
let elem : bits('SEW_widen) = match funct6 {
5247
IVV_VWREDSUMU => to_bits(SEW_widen, unsigned(vs2_val[i])),
5348
IVV_VWREDSUM => to_bits(SEW_widen, signed(vs2_val[i]))
5449
};
@@ -99,16 +94,12 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
9994

10095
if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
10196

102-
let 'n = num_elem_vs;
103-
let 'd = num_elem_vd;
104-
let 'm = SEW;
105-
106-
let vm_val : bits('n) = read_vmask(num_elem_vs, vm, zvreg);
107-
let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd);
108-
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
109-
let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
97+
let vm_val = read_vmask(num_elem_vs, vm, zvreg);
98+
let vd_val = read_vreg(num_elem_vd, SEW, 0, vd);
99+
let vs2_val = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
100+
let mask = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
110101

111-
var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
102+
var sum = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
112103
foreach (i from 0 to (num_elem_vs - 1)) {
113104
if mask[i] == bitone then {
114105
sum = match funct6 {

0 commit comments

Comments
 (0)