diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index f366c487a..22e3d936f 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -231,7 +231,7 @@ function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | extensionEnabled(Ex /* RV32Zdinx requires even register pairs; can be omitted for code */ /* not used for RV32Zdinx (i.e. RV64-only or D-only). */ -val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, dec, regidx)) -> bool +val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, regidx)) -> bool function validDoubleRegs(n, regs) = { if extensionEnabled(Ext_Zdinx) & sizeof(xlen) == 32 then foreach (i from 0 to (n - 1)) diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 1654f65f0..77376ed37 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -55,10 +55,10 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -122,7 +122,7 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { VV_VRGATHEREI16 => { if (vs1 == vd | vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; /* vrgatherei16.vv uses SEW/LMUL for the data in vs2 but EEW=16 and EMUL = (16/SEW)*LMUL for the indices in vs1 */ - let vs1_new : vector('n, dec, bits(16)) = read_vreg(num_elem, 16, 4 + LMUL_pow - SEW_pow, vs1); + let vs1_new : vector('n, bits(16)) = read_vreg(num_elem, 16, 4 + LMUL_pow - SEW_pow, vs1); let idx = unsigned(vs1_new[i]); let VLMAX = 2 ^ (LMUL_pow + VLEN_pow - SEW_pow); assert(VLMAX <= 'n); @@ -191,10 +191,10 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -257,10 +257,10 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -316,11 +316,11 @@ function clause execute(MASKTYPEV(vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); - 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); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + var result : vector('n, bits('m)) = vector_init(zeros()); let tail_ag : agtype = get_vtype_vta(); foreach (i from 0 to (num_elem - 1)) { @@ -361,9 +361,9 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -419,10 +419,10 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -539,10 +539,10 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -605,10 +605,10 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -670,10 +670,10 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -733,11 +733,11 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); 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); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + var result : vector('n, bits('m)) = vector_init(zeros()); let tail_ag : agtype = get_vtype_vta(); foreach (i from 0 to (num_elem - 1)) { @@ -779,8 +779,8 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let 'm = SEW; 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -828,10 +828,10 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -924,10 +924,10 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -990,10 +990,10 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1055,10 +1055,10 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1118,11 +1118,11 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); 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); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + var result : vector('n, bits('m)) = vector_init(zeros()); let tail_ag : agtype = get_vtype_vta(); foreach (i from 0 to (num_elem - 1)) { @@ -1163,9 +1163,9 @@ function clause execute(MOVETYPEI(vd, simm)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, 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); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1201,10 +1201,10 @@ function clause execute(VMVRTYPE(vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vd); + var result : vector('n, bits('m)) = vector_init(zeros()); foreach (i from 0 to (num_elem - 1)) { result[i] = if i < start_element then vd_val[i] else vs2_val[i] @@ -1256,10 +1256,10 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1364,10 +1364,10 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1429,10 +1429,10 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -1497,10 +1497,10 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -1560,10 +1560,10 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -1619,9 +1619,9 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { let 'm = SEW; let 'o = SEW_half; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1675,9 +1675,9 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { let 'm = SEW; let 'o = SEW_quart; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1731,9 +1731,9 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { let 'm = SEW; let 'o = SEW_eighth; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1777,7 +1777,7 @@ function clause execute(VMVXS(vs2, rd)) = { let 'n = num_elem; let 'm = SEW; - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); X(rd) = if sizeof(xlen) < SEW then slice(vs2_val[0], 0, sizeof(xlen)) else if sizeof(xlen) > SEW then sign_extend(vs2_val[0]) else vs2_val[0]; @@ -1809,10 +1809,10 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + let vs1_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + var result : vector('n, bits('m)) = vector_init(zeros()); /* body elements */ var vd_idx : nat = 0; @@ -1879,10 +1879,10 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1998,10 +1998,10 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -2063,10 +2063,10 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -2130,10 +2130,10 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -2193,10 +2193,10 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -2243,9 +2243,9 @@ function clause execute(VMVSX(rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, 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); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val); var result = initial_result; diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 72bdca226..89c82803f 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -42,10 +42,10 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -116,10 +116,10 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -188,10 +188,10 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -252,10 +252,10 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -314,10 +314,10 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -371,9 +371,9 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -489,9 +489,9 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -618,9 +618,9 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { let 'm = SEW; let 'o = SEW_widen; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -748,9 +748,9 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -823,7 +823,7 @@ function clause execute(VFMVFS(vs2, rd)) = { let 'n = num_elem; let 'm = SEW; - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); match 'm { 16 => F_H(rd) = vs2_val[0], 32 => F_S(rd) = vs2_val[0], @@ -871,10 +871,10 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -960,10 +960,10 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1031,10 +1031,10 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -1094,10 +1094,10 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -1155,10 +1155,10 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, 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); + let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; @@ -1207,11 +1207,11 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); 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); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + var result : vector('n, bits('m)) = vector_init(zeros()); let tail_ag : agtype = get_vtype_vta(); foreach (i from 0 to (num_elem - 1)) { @@ -1256,8 +1256,8 @@ function clause execute(VFMV(rs1, vd)) = { let 'm = SEW; 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -1291,9 +1291,9 @@ function clause execute(VFMVSF(rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, 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); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val); var result = initial_result; diff --git a/model/riscv_insts_vext_fp_red.sail b/model/riscv_insts_vext_fp_red.sail index 28f28ca00..1c4946b49 100755 --- a/model/riscv_insts_vext_fp_red.sail +++ b/model/riscv_insts_vext_fp_red.sail @@ -40,10 +40,10 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po let 'd = num_elem_vd; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); - let vd_val : vector('d, dec, bits('m)) = read_vreg(num_elem_vd, SEW, 0, 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); + let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); + let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { @@ -83,10 +83,10 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); - let vd_val : vector('d, dec, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, 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); + let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); + let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); 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)) { diff --git a/model/riscv_insts_vext_fp_utils.sail b/model/riscv_insts_vext_fp_utils.sail index 8d7ccf8af..19187c73a 100755 --- a/model/riscv_insts_vext_fp_utils.sail +++ b/model/riscv_insts_vext_fp_utils.sail @@ -466,7 +466,7 @@ function rsqrt7 (v, sub) = { 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) }; assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); - let table : vector(128, dec, int) = [ + let table : vector(128, int) = [ 52, 51, 50, 48, 47, 46, 44, 43, 42, 41, 40, 39, 38, 36, 35, 34, 33, 32, 31, 30, 30, 29, 28, 27, @@ -560,7 +560,7 @@ function recip7 (v, rm_3b, sub) = { 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) }; assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); - let table : vector(128, dec, int) = [ + let table : vector(128, int) = [ 127, 125, 123, 121, 119, 117, 116, 114, 112, 110, 109, 107, 105, 104, 102, 100, 99, 97, 96, 94, 93, 91, 90, 88, diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail index 6d578fad7..2fb4d3e81 100755 --- a/model/riscv_insts_vext_fp_vm.sail +++ b/model/riscv_insts_vext_fp_vm.sail @@ -37,10 +37,10 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -100,10 +100,10 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index 4bc6f3122..c586000cc 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -38,9 +38,9 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vs1_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs1); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val); var result = initial_result; @@ -95,8 +95,8 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { let 'n = num_elem; let 'm = SEW; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); @@ -129,8 +129,8 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { let 'n = num_elem; let 'm = SEW; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); @@ -166,9 +166,9 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); var result = initial_result; @@ -206,9 +206,9 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); var result = initial_result; @@ -246,9 +246,9 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); var result = initial_result; @@ -290,9 +290,9 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -329,8 +329,8 @@ function clause execute(VID_V(vm, vd)) = { let 'n = num_elem; let 'm = SEW; - 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 vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index b2fcc8c57..cba0d01a7 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -71,8 +71,8 @@ val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8} function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); @@ -137,8 +137,8 @@ val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let tail_ag : agtype = get_vtype_vta(); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); @@ -242,9 +242,9 @@ val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8} function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vs3_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); - let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); + let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { if vm_val[i] then { /* active segments */ @@ -311,8 +311,8 @@ val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8 function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); @@ -378,10 +378,10 @@ val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8 function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vs3_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); - let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { /* active segments */ @@ -448,9 +448,9 @@ val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); let width_type : word_width = size_bytes(EEW_data_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); - let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); + let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); let (result, mask) = init_masked_result(num_elem, nf * EEW_data_bytes * 8, EMUL_data_pow, vd_seg, vm_val); @@ -540,10 +540,10 @@ val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); let width_type : word_width = size_bytes(EEW_data_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); - let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); - let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_data_pow, vm_val); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs3_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); + let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); + let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_data_pow, vm_val); /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { @@ -756,7 +756,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { }; foreach (j from cur_field to (nf - 1)) { - let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(elem_per_reg, load_width_bytes * 8, 0, vs3 + to_bits(5, j)); + let vs3_val : vector('n, bits('b * 8)) = read_vreg(elem_per_reg, load_width_bytes * 8, 0, vs3 + to_bits(5, j)); foreach (i from 0 to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; @@ -822,7 +822,7 @@ val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), in function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { let width_type : word_width = BYTE; let start_element = get_start_element(); - let vd_or_vs3_val : vector('n, dec, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3); + let vd_or_vs3_val : vector('n, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3); foreach (i from start_element to (num_elem - 1)) { if i < evl then { /* active elements */ diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index d01dc0d4f..67e34d2c5 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -39,10 +39,10 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); - let vd_val : vector('d, dec, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, 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); + let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); + let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); 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)) { @@ -101,10 +101,10 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'd = num_elem_vd; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); - let vd_val : vector('d, dec, bits('m)) = read_vreg(num_elem_vd, SEW, 0, 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); + let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); + let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index eeec68124..5aa5bdff1 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -199,14 +199,14 @@ function get_end_element() = unsigned(vl) - 1 * vector2 is a "mask" vector that is true for an element if the corresponding element * in the result vector should be updated by the calling instruction */ -val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) +val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vector('n, bits('m)), vector('n, bool)) -> (vector('n, bits('m)), vector('n, bool)) function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); let tail_ag : agtype = get_vtype_vta(); let mask_ag : agtype = get_vtype_vma(); - var mask : vector('n, dec, bool) = undefined; - var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, bool) = undefined; + var result : vector('n, 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)); @@ -252,11 +252,11 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { * (vs3 for store and vs2 for reduction). There's no destination register to be masked. * In these cases, this function can be called to simply get the mask vector for vs (without the prepared vd result vector). */ -val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, dec, bool)) -> vector('n, dec, bool) +val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, bool)) -> vector('n, bool) function init_masked_source(num_elem, LMUL_pow, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); - var mask : vector('n, dec, bool) = undefined; + var mask : vector('n, 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)); @@ -286,12 +286,12 @@ function init_masked_source(num_elem, LMUL_pow, vm_val) = { /* Mask handling for carry functions that use masks as input/output */ /* Only prestart and tail elements are masked in a mask value */ -val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) +val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, bool)) -> (vector('n, bool), vector('n, bool)) function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { let start_element = get_start_element(); let end_element = get_end_element(); - var mask : vector('n, dec, bool) = undefined; - var result : vector('n, dec, bool) = undefined; + var mask : vector('n, bool) = undefined; + var result : vector('n, 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)); @@ -322,13 +322,13 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { } /* Mask handling for cmp functions that use masks as output */ -val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) +val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, bool), vector('n, bool)) -> (vector('n, bool), vector('n, bool)) 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(); - var mask : vector('n, dec, bool) = undefined; - var result : vector('n, dec, bool) = undefined; + var mask : vector('n, bool) = undefined; + var result : vector('n, 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)); @@ -369,12 +369,11 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { * Read multiple register groups and concatenate them in parallel * The whole segments with the same element index are combined together */ -val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, dec, bits('q * 'm)) +val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'm >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, bits('q * 'm)) 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); - var vreg_list : vector('q, dec, vector('n, dec, bits('m))) = undefined; - var result : vector('n, dec, bits('q * 'm)) = undefined; + var vreg_list : vector('q, vector('n, bits('m))) = vector_init(vector_init(zeros())); + var result : vector('n, bits('q * 'm)) = vector_init(zeros()); foreach (j from 0 to (nf - 1)) { vreg_list[j] = read_vreg(num_elem, SEW, LMUL_pow, vrid + to_bits(5, j * LMUL_reg)); }; diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 93ad7e7d2..e6f50cf89 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -35,10 +35,10 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); var result = initial_result; @@ -90,9 +90,9 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - 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); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); var result = initial_result; @@ -145,15 +145,15 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - var vec_trues : vector('n, dec, bool) = undefined; + var vec_trues : vector('n, bool) = undefined; foreach (i from 0 to (num_elem - 1)) { vec_trues[i] = true }; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues); var result = initial_result; @@ -206,10 +206,10 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - 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); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -269,10 +269,10 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); var result = initial_result; @@ -325,8 +325,8 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let 'm = SEW; 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); var result = initial_result; @@ -379,15 +379,15 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - var vec_trues : vector('n, dec, bool) = undefined; + var vec_trues : vector('n, bool) = undefined; foreach (i from 0 to (num_elem - 1)) { vec_trues[i] = true }; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues); var result = initial_result; @@ -442,10 +442,10 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; @@ -508,10 +508,10 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); var result = initial_result; @@ -561,8 +561,8 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let 'm = SEW; 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); var result = initial_result; @@ -612,15 +612,15 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - var vec_trues : vector('n, dec, bool) = undefined; + var vec_trues : vector('n, bool) = undefined; foreach (i from 0 to (num_elem - 1)) { vec_trues[i] = true }; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues); var result = initial_result; @@ -671,10 +671,10 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); 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); + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); var result = initial_result; diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 65afd2b4d..46ab8020c 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -40,8 +40,8 @@ bitfield Pmpcfg_ent : bits(8) = { R : 0 /* read */ } -register pmpcfg_n : vector(64, dec, Pmpcfg_ent) -register pmpaddr_n : vector(64, dec, xlenbits) +register pmpcfg_n : vector(64, Pmpcfg_ent) +register pmpaddr_n : vector(64, xlenbits) /* Packing and unpacking pmpcfg regs for xlen-width accesses */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index f825ce8cc..2291f2b0a 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -503,11 +503,11 @@ function retire_instruction() -> unit = { // HPM (Hardware Performance Monitoring) counters. The lowest three values are // not used but they are defined for simplicity. -register mhpmcounter : vector(32, dec, bits(64)) +register mhpmcounter : vector(32, bits(64)) // HPM events selector. These control what the HPM counters measure. The lowest // three values are not used but they are defined for simplicity. -register mhpmevent : vector(32, dec, xlenbits) +register mhpmevent : vector(32, xlenbits) // Valid HPM counter indices. The lowest three are used for mcycle, mtime and minstret. type hpmidx = range(3, 31) diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index f823155cc..aadd05bc2 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -239,10 +239,10 @@ function get_num_elem(LMUL_pow, SEW) = { } /* Reads a single vreg into multiple elements */ -val read_single_vreg : forall 'n 'm, 'n >= 0 & 'm >= 0. (int('n), int('m), regidx) -> vector('n, dec, bits('m)) +val read_single_vreg : forall 'n 'm, 'n >= 0 & 'm >= 0. (int('n), int('m), regidx) -> vector('n, bits('m)) function read_single_vreg(num_elem, SEW, vrid) = { let bv : vregtype = V(vrid); - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + var result : vector('n, bits('m)) = vector_init(zeros()); assert(8 <= SEW & SEW <= 64); foreach (i from 0 to (num_elem - 1)) { @@ -254,7 +254,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 +val write_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx, vector('n, bits('m))) -> unit function write_single_vreg(num_elem, SEW, vrid, v) = { var r : vregtype = zeros(); @@ -268,9 +268,9 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { } /* The general vreg reading operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m)) +val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, bits('m)) function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { - var result : vector('n, dec, bits('m)) = vector_init(zeros()); + var result : vector('n, bits('m)) = vector_init(zeros()); let VLEN = unsigned(vlenb) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; @@ -291,7 +291,7 @@ function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { let r_start_i : int = i_lmul * 'num_elem_single; let r_end_i : int = r_start_i + 'num_elem_single - 1; let vrid_lmul : regidx = vrid + to_bits(5, i_lmul); - let single_result : vector('num_elem_single, dec, bits('m)) = read_single_vreg('num_elem_single, SEW, vrid_lmul); + let single_result : vector('num_elem_single, bits('m)) = read_single_vreg('num_elem_single, SEW, vrid_lmul); foreach (r_i from r_start_i to r_end_i) { let s_i : int = r_i - r_start_i; assert(0 <= r_i & r_i < num_elem); @@ -314,13 +314,13 @@ function read_single_element(EEW, index, vrid) = { assert('elem_per_reg >= 0); let real_vrid : regidx = vrid + to_bits(5, index / 'elem_per_reg); 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); + let vrid_val : vector('elem_per_reg, bits('m)) = read_single_vreg('elem_per_reg, EEW, real_vrid); assert(0 <= real_index & real_index < 'elem_per_reg); vrid_val[real_index] } /* The general vreg writing operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val write_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, dec, bits('m))) -> unit +val write_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, bits('m))) -> unit function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { let VLEN = unsigned(vlenb) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; @@ -328,7 +328,7 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { let 'num_elem_single : int = VLEN / SEW; assert('num_elem_single >= 0); foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) { - var single_vec : vector('num_elem_single, dec, bits('m)) = vector_init(zeros()); + var single_vec : vector('num_elem_single, bits('m)) = vector_init(zeros()); let vrid_lmul : regidx = vrid + to_bits(5, i_lmul); let r_start_i : int = i_lmul * 'num_elem_single; let r_end_i : int = r_start_i + 'num_elem_single - 1; @@ -351,7 +351,7 @@ function write_single_element(EEW, index, vrid, value) = { let real_vrid : regidx = vrid + to_bits(5, index / 'elem_per_reg); 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); + let vrid_val : vector('elem_per_reg, bits('m)) = read_single_vreg('elem_per_reg, EEW, real_vrid); var r : vregtype = zeros(); foreach (i from ('elem_per_reg - 1) downto 0) { r = r << EEW; @@ -365,11 +365,11 @@ function write_single_element(EEW, index, vrid, value) = { } /* Mask register reading operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val read_vmask : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) +val read_vmask : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, bool) function read_vmask(num_elem, vm, vrid) = { assert(num_elem <= sizeof(vlenmax)); let vreg_val : vregtype = V(vrid); - var result : vector('n, dec, bool) = vector_init(true); + var result : vector('n, bool) = vector_init(true); if vm == 0b1 then { return result @@ -383,11 +383,11 @@ function read_vmask(num_elem, vm, vrid) = { } /* This is a special version of read_vmask for carry/borrow instructions, where vm=1 means no carry */ -val read_vmask_carry : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) +val read_vmask_carry : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, bool) function read_vmask_carry(num_elem, vm, vrid) = { assert(num_elem <= sizeof(vlenmax)); let vreg_val : vregtype = V(vrid); - var result : vector('n, dec, bool) = vector_init(false); + var result : vector('n, bool) = vector_init(false); if vm == 0b1 then { return result @@ -401,7 +401,7 @@ function read_vmask_carry(num_elem, vm, vrid) = { } /* Mask register writing operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, dec, bool)) -> unit +val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, bool)) -> unit function write_vmask(num_elem, vrid, v) = { let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax));