Skip to content

Commit

Permalink
Merge pull request #541 from Timmmm/user/timh/strict_var
Browse files Browse the repository at this point in the history 
Add explicit vars and enable --strict-var
  • Loading branch information
@billmcspadden-riscv
billmcspadden-riscv committed Sep 10, 2024
2 parents ad8b8cb + 3d1c9ab commit d905c9c
Show file tree
Hide file tree
Showing 15 changed files with 175 additions and 174 deletions.
1 change: 1 addition & 0 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,7 @@ SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SA

PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml)

SAIL_FLAGS += --strict-var
SAIL_FLAGS += -dno_cast
SAIL_DOC_FLAGS ?= -doc_embed plain

Expand Down
2 changes: 1 addition & 1 deletion model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ 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();
var ys : bits(8) = zeros();
foreach (i from 0 to 7)
ys[i] = xs[7-i];
ys
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_fetch.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ function fetch() -> FetchResult =
then F_RVC(ilo)
else {
/* fetch PC check for the next instruction granule */
PC_hi : xlenbits = PC + 2;
let PC_hi = PC + 2;
match ext_fetch_check_pc(PC, PC_hi) {
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc_hi) => {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_fetch_rvfi.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ function fetch() -> FetchResult = {
then F_RVC(i[15 .. 0])
else {
/* fetch PC check for the next instruction granule */
PC_hi : xlenbits = PC + 2;
let PC_hi = PC + 2;
match ext_fetch_check_pc(PC, PC_hi) {
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc_hi) =>
Expand Down
124 changes: 62 additions & 62 deletions model/riscv_insts_vext_arith.sail
View file

Large diffs are not rendered by default.

66 changes: 33 additions & 33 deletions model/riscv_insts_vext_fp.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = {
let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -121,8 +121,8 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -194,8 +194,8 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = {
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -259,8 +259,8 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = {
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -322,8 +322,8 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = {
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -379,8 +379,8 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -498,8 +498,8 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -628,8 +628,8 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -759,8 +759,8 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -884,8 +884,8 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = {
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -974,8 +974,8 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = {
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -1046,8 +1046,8 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = {
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -1110,8 +1110,8 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = {
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -1172,8 +1172,8 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = {
let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
result : vector('n, dec, bits('o)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('o)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);

Expand Down Expand Up @@ -1225,7 +1225,7 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = {
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
var result : vector('n, dec, bits('m)) = undefined;

let tail_ag : agtype = get_vtype_vta();
foreach (i from 0 to (num_elem - 1)) {
Expand Down Expand Up @@ -1272,8 +1272,8 @@ function clause execute(VFMV(rs1, vd)) = {
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -1309,8 +1309,8 @@ function clause execute(VFMVSF(rs1, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000);
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);

Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_vext_fp_red.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
let mask : vector('n, dec, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);

sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
foreach (i from 0 to (num_elem_vs - 1)) {
if mask[i] then {
sum = match funct6 {
Expand Down Expand Up @@ -88,7 +88,7 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
let mask : vector('n, dec, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);

sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
foreach (i from 0 to (num_elem_vs - 1)) {
if mask[i] then {
/* currently ordered/unordered sum reductions do the same operations */
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_vext_fp_vm.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down Expand Up @@ -105,8 +105,8 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down
44 changes: 22 additions & 22 deletions model/riscv_insts_vext_mask.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
let vs1_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs1);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val);

Expand Down Expand Up @@ -98,12 +98,12 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = {

let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);

count : nat = 0;
var count : nat = 0;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] & vs2_val[i] then count = count + 1;
};
Expand Down Expand Up @@ -134,12 +134,12 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = {

let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);

index : int = -1;
var index : int = -1;
foreach (i from 0 to (num_elem - 1)) {
if index == -1 then {
if mask[i] & vs2_val[i] then index = i;
Expand Down Expand Up @@ -174,12 +174,12 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);

found_elem : bool = false;
var found_elem : bool = false;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
if vs2_val[i] then found_elem = true;
Expand Down Expand Up @@ -215,12 +215,12 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);

found_elem : bool = false;
var found_elem : bool = false;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = if found_elem then false else true;
Expand Down Expand Up @@ -256,12 +256,12 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bool) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);

found_elem : bool = false;
var found_elem : bool = false;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
if vs2_val[i] & not(found_elem) then {
Expand Down Expand Up @@ -301,12 +301,12 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = {
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

sum : int = 0;
var sum : int = 0;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = to_bits(SEW, sum);
Expand Down Expand Up @@ -340,8 +340,8 @@ function clause execute(VID_V(vm, vd)) = {

let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
mask : vector('n, dec, bool) = undefined;
var result : vector('n, dec, bits('m)) = undefined;
var mask : vector('n, dec, bool) = undefined;

(result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);

Expand Down
Loading

0 comments on commit d905c9c

Please sign in to comment.