From 3d1c9ab113da773f9d3ed2d8f9e69c0fbc8df10d Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 4 Sep 2024 18:43:46 +0100 Subject: [PATCH] Add explicit vars and enable --strict-var This adds explicit `var` keywords where they were missing before, and enables the `--strict-var` flag to prevent us from missing them out in future. Implicit `var` was a mistake inherited from ASL. --- Makefile | 1 + model/prelude.sail | 2 +- model/riscv_fetch.sail | 2 +- model/riscv_fetch_rvfi.sail | 2 +- model/riscv_insts_vext_arith.sail | 124 ++++++++++++++--------------- model/riscv_insts_vext_fp.sail | 66 +++++++-------- model/riscv_insts_vext_fp_red.sail | 4 +- model/riscv_insts_vext_fp_vm.sail | 8 +- model/riscv_insts_vext_mask.sail | 44 +++++----- model/riscv_insts_vext_mem.sail | 10 +-- model/riscv_insts_vext_red.sail | 4 +- model/riscv_insts_vext_utils.sail | 20 ++--- model/riscv_insts_vext_vm.sail | 54 ++++++------- model/riscv_step.sail | 4 +- model/riscv_vext_regs.sail | 4 +- 15 files changed, 175 insertions(+), 174 deletions(-) diff --git a/Makefile b/Makefile index 13e55a720..8cda2816b 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/model/prelude.sail b/model/prelude.sail index 3555296b3..c924a2f53 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -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 diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 480f47e2e..170c38712 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -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) => { diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index ab09d26e1..b81d43915 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -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) => diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 14700ca34..b832dcf49 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -59,8 +59,8 @@ function clause execute(VVTYPE(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); @@ -196,8 +196,8 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, 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('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); @@ -263,8 +263,8 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, 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('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); @@ -323,7 +323,7 @@ function clause execute(MASKTYPEV(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; + var result : vector('n, dec, bits('m)) = undefined; let tail_ag : agtype = get_vtype_vta(); foreach (i from 0 to (num_elem - 1)) { @@ -367,8 +367,8 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); 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); @@ -427,8 +427,8 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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); @@ -548,8 +548,8 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - 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); @@ -615,8 +615,8 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - 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); @@ -681,8 +681,8 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let rs1_val : nat = unsigned(X(rs1)); 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); @@ -745,7 +745,7 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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)) { @@ -789,8 +789,8 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let rs1_val : bits('m) = get_scalar(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); @@ -841,8 +841,8 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); 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); @@ -938,8 +938,8 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - 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); @@ -1005,8 +1005,8 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - 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); @@ -1071,8 +1071,8 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let imm_val : nat = unsigned(zero_extend(sizeof(xlen), simm)); 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); @@ -1135,7 +1135,7 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); 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)) { @@ -1179,8 +1179,8 @@ function clause execute(MOVETYPEI(vd, simm)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let imm_val : bits('m) = sign_extend(simm); 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); @@ -1218,7 +1218,7 @@ function clause execute(VMVRTYPE(vs2, simm, vd)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vd); - result : vector('n, dec, bits('m)) = undefined; + var result : vector('n, dec, bits('m)) = undefined; foreach (i from 0 to (num_elem - 1)) { result[i] = if i < start_element then vd_val[i] else vs2_val[i] @@ -1274,8 +1274,8 @@ function clause execute(MVVTYPE(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); @@ -1383,8 +1383,8 @@ function clause execute(MVVMATYPE(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); @@ -1449,8 +1449,8 @@ function clause execute(WVVTYPE(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); @@ -1518,8 +1518,8 @@ function clause execute(WVTYPE(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); @@ -1582,8 +1582,8 @@ function clause execute(WMVVTYPE(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); @@ -1641,8 +1641,8 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, 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); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2); - 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); @@ -1699,8 +1699,8 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, 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); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2); - 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); @@ -1757,8 +1757,8 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, 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); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2); - 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); @@ -1836,10 +1836,10 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { let vs1_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 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; + var result : vector('n, dec, bits('m)) = undefined; /* body elements */ - vd_idx : nat = 0; + var vd_idx : nat = 0; foreach (i from 0 to (num_elem - 1)) { if i <= end_element then { if vs1_val[i] then { @@ -1907,8 +1907,8 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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); @@ -2027,8 +2027,8 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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); @@ -2093,8 +2093,8 @@ function clause execute(WVXTYPE(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(rs1, SEW); 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); @@ -2161,8 +2161,8 @@ function clause execute(WXTYPE(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(rs1, SEW); 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); @@ -2225,8 +2225,8 @@ function clause execute(WMVXTYPE(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(rs1, SEW); 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); @@ -2275,8 +2275,8 @@ function clause execute(VMVSX(rs1, vd)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let rs1_val : bits('m) = get_scalar(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); diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 945199da8..83006d1ef 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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); @@ -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)) { @@ -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); @@ -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); diff --git a/model/riscv_insts_vext_fp_red.sail b/model/riscv_insts_vext_fp_red.sail index 9d4220da1..28f28ca00 100755 --- a/model/riscv_insts_vext_fp_red.sail +++ b/model/riscv_insts_vext_fp_red.sail @@ -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 { @@ -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 */ diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail index 55592c4a8..1914ed74b 100755 --- a/model/riscv_insts_vext_fp_vm.sail +++ b/model/riscv_insts_vext_fp_vm.sail @@ -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); @@ -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); diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index 241e210fd..9c536bb0a 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -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); @@ -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; }; @@ -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; @@ -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; @@ -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; @@ -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 { @@ -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); @@ -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); diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 449d600a9..b2fcc8c57 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -143,7 +143,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); - trimmed : bool = false; + var trimmed : bool = false; foreach (i from 0 to (num_elem - 1)) { if not(trimmed) then { if vm_val[i] then { /* active segments */ @@ -637,8 +637,8 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { let start_element = get_start_element(); if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ let elem_to_align : int = start_element % elem_per_reg; - cur_field : int = start_element / elem_per_reg; - cur_elem : int = start_element; + var cur_field : int = start_element / elem_per_reg; + var cur_elem : int = start_element; if elem_to_align > 0 then { foreach (i from elem_to_align to (elem_per_reg - 1)) { @@ -719,8 +719,8 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { let start_element = get_start_element(); if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ let elem_to_align : int = start_element % elem_per_reg; - cur_field : int = start_element / elem_per_reg; - cur_elem : int = start_element; + var cur_field : int = start_element / elem_per_reg; + var cur_elem : int = start_element; if elem_to_align > 0 then { foreach (i from elem_to_align to (elem_per_reg - 1)) { diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 2ce2f2c47..d01dc0d4f 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -44,7 +44,7 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { 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 { let elem : bits('o) = match funct6 { @@ -106,7 +106,7 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { 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 { diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 4bf570671..87cb38677 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -205,8 +205,8 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { let end_element = get_end_element(); let tail_ag : agtype = get_vtype_vta(); let mask_ag : agtype = get_vtype_vma(); - mask : vector('n, dec, bool) = undefined; - result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + var result : vector('n, dec, bits('m)) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -256,7 +256,7 @@ val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, de function init_masked_source(num_elem, LMUL_pow, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); - mask : vector('n, dec, bool) = undefined; + var mask : vector('n, dec, bool) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -290,8 +290,8 @@ val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int( function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { let start_element = get_start_element(); let end_element = get_end_element(); - mask : vector('n, dec, bool) = undefined; - result : vector('n, dec, bool) = undefined; + var mask : vector('n, dec, bool) = undefined; + var result : vector('n, dec, bool) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -327,8 +327,8 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); let mask_ag : agtype = get_vtype_vma(); - mask : vector('n, dec, bool) = undefined; - result : vector('n, dec, bool) = undefined; + var mask : vector('n, dec, bool) = undefined; + var result : vector('n, dec, bool) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -373,8 +373,8 @@ val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'q >= 0. (int('n), int('m), in function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { assert('q * 'm > 0); let LMUL_reg : int = if LMUL_pow <= 0 then 1 else 2 ^ (LMUL_pow); - vreg_list : vector('q, dec, vector('n, dec, bits('m))) = undefined; - result : vector('n, dec, bits('q * 'm)) = undefined; + var vreg_list : vector('q, dec, vector('n, dec, bits('m))) = undefined; + var result : vector('n, dec, bits('q * 'm)) = undefined; foreach (j from 0 to (nf - 1)) { vreg_list[j] = read_vreg(num_elem, SEW, LMUL_pow, vrid + to_bits(5, j * LMUL_reg)); }; @@ -441,7 +441,7 @@ function signed_saturation(len, elem) = { val count_leadingzeros : (bits(64), int) -> int function count_leadingzeros (sig, len) = { - idx : int = -1; + var idx : int = -1; assert(len == 10 | len == 23 | len == 52); foreach (i from 0 to (len - 1)) { if sig[i] == bitone then idx = i; diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 91ce3f361..e524b75bc 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -39,8 +39,8 @@ function clause execute(VVMTYPE(funct6, 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_carry(num_elem, SEW, LMUL_pow, vd_val); @@ -94,8 +94,8 @@ function clause execute(VVMCTYPE(funct6, 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_carry(num_elem, SEW, LMUL_pow, vd_val); @@ -147,7 +147,7 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - vec_trues : vector('n, dec, bool) = undefined; + var vec_trues : vector('n, dec, bool) = undefined; foreach (i from 0 to (num_elem - 1)) { vec_trues[i] = true }; @@ -156,8 +156,8 @@ function clause execute(VVMSTYPE(funct6, 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, vec_trues); @@ -213,8 +213,8 @@ function clause execute(VVCMPTYPE(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); @@ -277,8 +277,8 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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_carry(num_elem, SEW, LMUL_pow, vd_val); @@ -332,8 +332,8 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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_carry(num_elem, SEW, LMUL_pow, vd_val); @@ -385,7 +385,7 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - vec_trues : vector('n, dec, bool) = undefined; + var vec_trues : vector('n, dec, bool) = undefined; foreach (i from 0 to (num_elem - 1)) { vec_trues[i] = true }; @@ -394,8 +394,8 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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, vec_trues); @@ -453,8 +453,8 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); 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); @@ -520,8 +520,8 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); 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_carry(num_elem, SEW, LMUL_pow, vd_val); @@ -572,8 +572,8 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); 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_carry(num_elem, SEW, LMUL_pow, vd_val); @@ -622,7 +622,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - vec_trues : vector('n, dec, bool) = undefined; + var vec_trues : vector('n, dec, bool) = undefined; foreach (i from 0 to (num_elem - 1)) { vec_trues[i] = true }; @@ -631,8 +631,8 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); 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, vec_trues); @@ -686,8 +686,8 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); 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); diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 8e8e47816..21bd82e47 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -93,8 +93,8 @@ function step(step_no : int) -> bool = { function loop () : unit -> unit = { let insns_per_tick = plat_insns_per_tick(); - i : int = 0; - step_no : int = 0; + var i : int = 0; + var step_no : int = 0; while not(htif_done) do { let stepped = step(step_no); if stepped then { diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 511e2aca1..377d92d51 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -262,7 +262,7 @@ function read_single_vreg(num_elem, SEW, vrid) = { /* Writes multiple elements into a single vreg */ val write_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx, vector('n, dec, bits('m))) -> unit function write_single_vreg(num_elem, SEW, vrid, v) = { - r : vregtype = zeros(); + var r : vregtype = zeros(); assert(8 <= SEW & SEW <= 64); foreach (i from (num_elem - 1) downto 0) { @@ -358,7 +358,7 @@ function write_single_element(EEW, index, vrid, value) = { let real_index : int = index % 'elem_per_reg; let vrid_val : vector('elem_per_reg, dec, bits('m)) = read_single_vreg('elem_per_reg, EEW, real_vrid); - r : vregtype = zeros(); + var r : vregtype = zeros(); foreach (i from ('elem_per_reg - 1) downto 0) { r = r << EEW; if i == real_index then {