diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 915a9fdfa..86e5da6df 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -1405,7 +1405,6 @@ mapping clause encdec = MVVMATYPE(funct6, vm, vs2, vs1, vd) if haveRVV() function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let VLEN = int_power(2, get_vlen_pow()); let num_elem = get_num_elem(LMUL_pow, SEW); if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; @@ -1422,7 +1421,6 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); - assert(VLEN >= 0); foreach (i from 0 to (num_elem - 1)){ if mask[i] then{ result[i] = match funct6 { @@ -1487,7 +1485,6 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { result : vector('n, dec, bits('o)) = undefined; mask : vector('n, dec, bool) = undefined; - assert(8 <= SEW_widen & SEW_widen <= 64); (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -1557,7 +1554,6 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { result : vector('n, dec, bits('o)) = undefined; mask : vector('n, dec, bool) = undefined; - assert(8 <= SEW_widen & SEW_widen <= 64); (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -1622,7 +1618,6 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { result : vector('n, dec, bits('o)) = undefined; mask : vector('n, dec, bool) = undefined; - assert(8 <= SEW_widen & SEW_widen <= 64); (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -2053,7 +2048,6 @@ mapping clause encdec = MVXMATYPE(funct6, vm, vs2, rs1, vd) if haveRVV() function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let VLEN = int_power(2, get_vlen_pow()); let num_elem = get_num_elem(LMUL_pow, SEW); if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; @@ -2070,7 +2064,6 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); - assert(VLEN >= 0); foreach (i from 0 to (num_elem - 1)){ if mask[i] then{ result[i] = match funct6 { @@ -2135,7 +2128,6 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { result : vector('n, dec, bits('o)) = undefined; mask : vector('n, dec, bool) = undefined; - assert(8 <= SEW_widen & SEW_widen <= 64); (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -2204,7 +2196,6 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { result : vector('n, dec, bits('o)) = undefined; mask : vector('n, dec, bool) = undefined; - assert(8 <= SEW_widen & SEW_widen <= 64); (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -2269,7 +2260,6 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { result : vector('n, dec, bits('o)) = undefined; mask : vector('n, dec, bool) = undefined; - assert(8 <= SEW_widen & SEW_widen <= 64); (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 2e0e2570d..b2871f49b 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -90,9 +90,9 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { FVV_VMAX => fp_max(vs2_val[i], vs1_val[i]), FVV_VMUL => fp_mul(rm_3b, vs2_val[i], vs1_val[i]), FVV_VDIV => fp_div(rm_3b, vs2_val[i], vs1_val[i]), - FVV_VSGNJ => vs1_val[i][('m - 1)..('m - 1)] @ vs2_val[i][('m - 2)..0], - FVV_VSGNJN => (0b1 ^ vs1_val[i][('m - 1)..('m - 1)]) @ vs2_val[i][('m - 2)..0], - FVV_VSGNJX => (vs2_val[i][('m - 1)..('m - 1)] ^ vs1_val[i][('m - 1)..('m - 1)]) @ vs2_val[i][('m - 2)..0] + FVV_VSGNJ => [vs1_val[i]['m - 1]] @ vs2_val[i][('m - 2)..0], + FVV_VSGNJN => (0b1 ^ [vs1_val[i]['m - 1]]) @ vs2_val[i][('m - 2)..0], + FVV_VSGNJX => ([vs2_val[i]['m - 1]] ^ [vs1_val[i]['m - 1]]) @ vs2_val[i][('m - 2)..0] } } }; @@ -932,9 +932,9 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { VF_VMUL => fp_mul(rm_3b, vs2_val[i], rs1_val), VF_VDIV => fp_div(rm_3b, vs2_val[i], rs1_val), VF_VRDIV => fp_div(rm_3b, rs1_val, vs2_val[i]), - VF_VSGNJ => rs1_val[('m - 1)..('m - 1)] @ vs2_val[i][('m - 2)..0], - VF_VSGNJN => (0b1 ^ rs1_val[('m - 1)..('m - 1)]) @ vs2_val[i][('m - 2)..0], - VF_VSGNJX => (vs2_val[i][('m - 1)..('m - 1)] ^ rs1_val[('m - 1)..('m - 1)]) @ vs2_val[i][('m - 2)..0], + VF_VSGNJ => [rs1_val['m - 1]] @ vs2_val[i][('m - 2)..0], + VF_VSGNJN => (0b1 ^ [rs1_val['m - 1]]) @ vs2_val[i][('m - 2)..0], + VF_VSGNJX => ([vs2_val[i]['m - 1]] ^ [rs1_val['m - 1]]) @ vs2_val[i][('m - 2)..0], VF_VSLIDE1UP => { if vs2 == vd then { handle_illegal(); return RETIRE_FAIL }; if i == 0 then rs1_val else vs2_val[i - 1] diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 796ea4ad8..30ed6ac0b 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -109,39 +109,35 @@ function process_vle (vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); - total : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - status : Retired = RETIRE_SUCCESS; - (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); + let (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = i * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => total[i] = result, - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + if mask[i] then { /* active elements */ + vstart = to_bits(16, i); + let elem_offset = i * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { + MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } + } } + } else { /* prestart, masked or tail elements */ + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, total[i]) } }; - if status == RETIRE_SUCCESS then write_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd, total); vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLETYPE(vm, rs1, width, vd)) = { @@ -179,46 +175,40 @@ function process_vse (vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vs3); - total : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - status : Retired = RETIRE_SUCCESS; - - (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vs3_val, vm_val); + let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = i * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + if mask[i] then { /* active elements */ + vstart = to_bits(16, i); + let elem_offset = i * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSETYPE(vm, rs1, width, vs3)) = { @@ -257,39 +247,35 @@ function process_vlse (vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); - total : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - status : Retired = RETIRE_SUCCESS; - (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); + let (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = i * rs2_val; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => total[i] = result, - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + if mask[i] then { /* active elements */ + vstart = to_bits(16, i); + let elem_offset = i * rs2_val; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { + MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } + } } + } else { /* prestart, masked or tail elements */ + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, total[i]) } }; - if status == RETIRE_SUCCESS then write_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd, total); vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLSETYPE(vm, rs2, rs1, width, vd)) = { @@ -328,46 +314,40 @@ function process_vsse (vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vs3); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); - total : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - status : Retired = RETIRE_SUCCESS; - - (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vs3_val, vm_val); + let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = i * rs2_val; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + if mask[i] then { /* active elements */ + vstart = to_bits(16, i); + let elem_offset = i * rs2_val; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSSETYPE(vm, rs2, rs1, width, vs3)) = { @@ -406,39 +386,36 @@ function process_vlxei (vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); - total : vector('n, dec, bits('db * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (total, mask) = init_masked_result(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd_val, vm_val); - status : Retired = RETIRE_SUCCESS; - /* Currently mop = 1(unordered) or 3(ordered) do the same operations */ + let (total, mask) = init_masked_result(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd_val, vm_val); + + /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = signed(vs2_val[i]); - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) then - { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { - MemValue(result) => total[i] = result, - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + if mask[i] then { /* active elements */ + vstart = to_bits(16, i); + let elem_offset = signed(vs2_val[i]); + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) then + { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { + MemValue(result) => write_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vd, result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } + } } + } else { /* prestart, masked or tail elements */ + write_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vd, total[i]) } }; - if status == RETIRE_SUCCESS then write_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd, total); vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLUXEITYPE(vm, vs2, rs1, width, vd)) = { @@ -493,46 +470,41 @@ function process_vsxei (vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vs3); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); - total : vector('n, dec, bits('db * 8)) = undefined; /* just used to generate mask */ - mask : vector('n, dec, bool) = undefined; - (total, mask) = init_masked_result(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vs3_val, vm_val); - status : Retired = RETIRE_SUCCESS; + let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_data_pow, vm_val); - /* Currently mop = 1(unordered) or 3(ordered) do the same operations */ + /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = signed(vs2_val[i]); - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, vs3_val[i], false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + if mask[i] then { /* active elements */ + vstart = to_bits(16, i); + let elem_offset = signed(vs2_val[i]); + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, vs3_val[i], false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSUXEITYPE(vm, vs2, rs1, width, vs3)) = { @@ -586,54 +558,50 @@ function process_vleff (vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); - total : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); - status : Retired = RETIRE_SUCCESS; + let tail_ag : agtype = get_vtype_vta(); + let (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); + + trimmed : bool = false; foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { + if not(trimmed) then { + if mask[i] then { /* active elements */ let elem_offset = i * load_width_bytes; match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { Ext_DataAddr_Error(e) => { - if i == 0 then { - ext_handle_data_check_error(e); - status = RETIRE_FAIL - } else { + if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } }, Ext_DataAddr_OK(vaddr) => { if check_misaligned(vaddr, width_type) then { - if i == 0 then { - handle_mem_exception(vaddr, E_Load_Addr_Align()); - status = RETIRE_FAIL - } else { + if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { - if i == 0 then { - handle_mem_exception(vaddr, e); - status = RETIRE_FAIL - } else { + if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => total[i] = result, + MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, result), MemException(e) => { - if i == 0 then { - handle_mem_exception(vaddr, e); - status = RETIRE_FAIL - } else { + if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } } } @@ -641,13 +609,20 @@ function process_vleff (vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { } } } + } else { /* prestart, masked or tail elements */ + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, total[i]) + } + } else { + /* if vl is trimmed, elements past the new vl are treated as tail elements */ + if tail_ag == AGNOSTIC then { + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd, vd_val[i]) + /* TODO: configuration support for agnostic behavior */ } } }; - if status == RETIRE_SUCCESS then write_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd, total); vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLEFFTYPE(vm, rs1, width, vd)) = { @@ -685,48 +660,41 @@ 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - status : Retired = RETIRE_SUCCESS; - vd_a = vd; - vd_t = vd; - - foreach(a from 0 to (nf - 1)) { - if vd_t == vd_a & a != 0 then vd_t = vd_t + 1; /* EMUL < 1 */ - let vd_t_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd_t); - total : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (total, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_t_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if mask[i] then { - vstart = to_bits(16, i); - let elem_offset = load_width_bytes * (a + i * nf); - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => total[i] = result, - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); + + let (total, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { /* active segments */ + vstart = to_bits(16, i); + foreach (j from 0 to (nf - 1)) { + let elem_offset = (i * nf + j) * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { + MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } + } } } - }; - - if status == RETIRE_SUCCESS then write_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd_t, total); - vd_a = vd_t; - vd_t = vd_t + to_bits(5, EMUL_reg) + } else { /* prestart, masked or tail segments */ + foreach (j from 0 to (nf - 1)) { + let elem_val = (total[i] >> (j * load_width_bytes * 8))[(load_width_bytes * 8 - 1) .. 0]; + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), elem_val) + } + } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLSEGTYPE(nf, vm, rs1, width, vd)) = { @@ -739,7 +707,7 @@ function clause execute(VLSEGTYPE(nf, vm, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); /* # of element of each register group */ let nf_int = nfields_int(nf); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_load(vd, vm, nf_int, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlseg(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -757,55 +725,53 @@ 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); - let start_element = get_start_element(); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - status : Retired = RETIRE_SUCCESS; - if start_element >= num_elem then return status; + let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); + let tail_ag : agtype = get_vtype_vta(); - foreach (i from start_element to (num_elem - 1)) { - if status != RETIRE_FAIL then { - if vm_val[i] then { + let (total, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); + + trimmed : bool = false; + foreach (i from 0 to (num_elem - 1)) { + if not(trimmed) then { + if vm_val[i] then { /* active segments */ foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { Ext_DataAddr_Error(e) => { - if i == 0 then { - ext_handle_data_check_error(e); - status = RETIRE_FAIL - } else { + if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } }, Ext_DataAddr_OK(vaddr) => { if check_misaligned(vaddr, width_type) then { - if i == 0 then { - handle_mem_exception(vaddr, E_Load_Addr_Align()); - status = RETIRE_FAIL - } else { + if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { - if i == 0 then { - handle_mem_exception(vaddr, e); - status = RETIRE_FAIL - } else { + if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), result), MemException(e) => { - if i == 0 then { - handle_mem_exception(vaddr, e); - status = RETIRE_FAIL - } else { + if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + else { vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)) + print_reg("CSR vl <- " ^ BitStr(vl)); + trimmed = true } } } @@ -814,12 +780,26 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } } } + } else { /* prestart, masked or tail segments */ + foreach (j from 0 to (nf - 1)) { + let elem_val = (total[i] >> (j * load_width_bytes * 8))[(load_width_bytes * 8 - 1) .. 0]; + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), elem_val) + } + } + } else { + /* if vl is trimmed, elements past the new vl are treated as tail elements */ + if tail_ag == AGNOSTIC then { + foreach (j from 0 to (nf - 1)) { + let elem_val = (vd_seg[i] >> (j * load_width_bytes * 8))[(load_width_bytes * 8 - 1) .. 0]; + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), elem_val) + } + /* TODO: configuration support for agnostic behavior */ } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLSEGFFTYPE(nf, vm, rs1, width, vd)) = { @@ -832,7 +812,7 @@ function clause execute(VLSEGFFTYPE(nf, vm, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_load(vd, vm, nf_int, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlsegff(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -850,48 +830,45 @@ 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); - let start_element = get_start_element(); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - status : Retired = RETIRE_SUCCESS; - if start_element >= num_elem then return status; + 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); - foreach (i from start_element to (num_elem - 1)) { - if vm_val[i] then { + foreach (i from 0 to (num_elem - 1)) { + if vm_val[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - if status != RETIRE_FAIL then { - let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let one_elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, EMUL_pow, vs3 + to_bits(5, j * EMUL_reg)); - let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, one_elem_val, false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + let elem_offset = (i * nf + j) * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, EMUL_pow, vs3 + to_bits(5, j * EMUL_reg)); + let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSSEGTYPE(nf, vm, rs1, width, vs3)) = { @@ -904,7 +881,7 @@ function clause execute(VSSEGTYPE(nf, vm, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_store(nf_int, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vsseg(nf_int, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -922,42 +899,43 @@ 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); /* only to generate mask */ - result : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (result, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vd_val, vm_val); - + 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 rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); - status : Retired = RETIRE_SUCCESS; + + let (total, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); + foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - if status != RETIRE_FAIL then { - let elem_offset = i * rs2_val + j * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg) , result), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + let elem_offset = i * rs2_val + j * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { + MemValue(result) => write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } + } } } + } else { /* prestart, masked or tail segments */ + foreach (j from 0 to (nf - 1)) { + let elem_val = (total[i] >> (j * load_width_bytes * 8))[(load_width_bytes * 8 - 1) .. 0]; + write_single_element(load_width_bytes * 8, i, EMUL_pow, vd + to_bits(5, j * EMUL_reg), elem_val) + } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLSSEGTYPE(nf, vm, rs2, rs1, width, vd)) = { @@ -970,7 +948,7 @@ function clause execute(VLSSEGTYPE(nf, vm, rs2, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_load(vd, vm, nf_int, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlsseg(nf_int, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -989,50 +967,45 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vs3); /* only to generate mask */ - result : vector('n, dec, bits('b * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (result, mask) = init_masked_result(num_elem, load_width_bytes * 8, EMUL_pow, vs3_val, vm_val); - + let vs3_seg : vector('n, dec, 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))); - status : Retired = RETIRE_SUCCESS; + let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - if status != RETIRE_FAIL then { - let elem_offset = i * rs2_val + j * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let one_elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, EMUL_pow, vs3 + to_bits(5, j * EMUL_reg)); - let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, one_elem_val, false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + let elem_offset = i * rs2_val + j * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, EMUL_pow, vs3 + to_bits(5, j * EMUL_reg)); + let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3)) = { @@ -1045,7 +1018,7 @@ function clause execute(VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_store(nf_int, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vssseg(nf_int, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -1064,42 +1037,43 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else int_power(2, EMUL_data_pow); let width_type : word_width = bytes_wordwidth(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd); + 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); - total : vector('n, dec, bits('db * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (total, mask) = init_masked_result(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd_val, vm_val); - status : Retired = RETIRE_SUCCESS; - /* Currently mop = 1(unordered) or 3(ordered) do the same operations */ + let (total, mask) = init_masked_result(num_elem, nf * EEW_data_bytes * 8, EMUL_data_pow, vd_seg, vm_val); + + /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - if status != RETIRE_FAIL then { - let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { - MemValue(result) => write_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vd + to_bits(5, j * EMUL_data_reg) , result), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { + MemValue(result) => write_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vd + to_bits(5, j * EMUL_data_reg), result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } + } } } + } else { /* prestart, masked or tail segments */ + foreach (j from 0 to (nf - 1)) { + let elem_val = (total[i] >> (j * EEW_data_bytes * 8))[(EEW_data_bytes * 8 - 1) .. 0]; + write_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vd + to_bits(5, j * EMUL_data_reg), elem_val) + } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { @@ -1112,7 +1086,7 @@ function clause execute(VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); let nf_int = nfields_int(nf); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_load(vd, vm, nf_int, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlxseg(nf_int, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) } @@ -1136,7 +1110,7 @@ function clause execute(VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); let nf_int = nfields_int(nf); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_load(vd, vm, nf_int, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlxseg(nf_int, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) } @@ -1155,51 +1129,46 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else int_power(2, EMUL_data_pow); let width_type : word_width = bytes_wordwidth(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vs3_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vs3); + 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); - total : vector('n, dec, bits('db * 8)) = undefined; - mask : vector('n, dec, bool) = undefined; - (total, mask) = init_masked_result(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vs3_val, vm_val); - status : Retired = RETIRE_SUCCESS; + let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_data_pow, vm_val); - /* Currently mop = 1(unordered) or 3(ordered) do the same operations */ + /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - if status != RETIRE_FAIL then { - let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let one_elem_val : bits('db * 8) = read_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vs3 + to_bits(5, j * EMUL_data_reg)); - let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, one_elem_val, false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let elem_val : bits('db * 8) = read_single_element(EEW_data_bytes * 8, i, EMUL_data_pow, vs3 + to_bits(5, j * EMUL_data_reg)); + let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, elem_val, false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { @@ -1212,7 +1181,7 @@ function clause execute(VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); /* number of data and indices are the same */ let nf_int = nfields_int(nf); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_store(nf_int, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vsxseg(nf_int, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) } @@ -1236,7 +1205,7 @@ function clause execute(VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); /* number of data and indices are the same */ let nf_int = nfields_int(nf); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_segment_store(nf_int, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vsxseg(nf_int, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) } @@ -1253,65 +1222,61 @@ mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if haveRVV() val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); - status : Retired = RETIRE_SUCCESS; - start_element = get_start_element(); - if start_element >= nf * elem_per_reg then return status; /* no elements are written */ + 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; - elem_to_align : int = start_element % elem_per_reg; + cur_elem : int = start_element; if elem_to_align > 0 then { foreach (i from elem_to_align to (elem_per_reg - 1)) { - if status != RETIRE_FAIL then { - vstart = to_bits(16, start_element); - let elem_offset : int = start_element * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => write_single_element(load_width_bytes * 8, i, 0, vd + to_bits(5, cur_field) , result), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + vstart = to_bits(16, cur_elem); + let elem_offset = cur_elem * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { + MemValue(result) => write_single_element(load_width_bytes * 8, i, 0, vd + to_bits(5, cur_field), result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - }; - start_element = start_element + 1 - } + } + }; + cur_elem = cur_elem + 1 }; cur_field = cur_field + 1 }; foreach (j from cur_field to (nf - 1)) { foreach (i from 0 to (elem_per_reg - 1)) { - if status != RETIRE_FAIL then { - vstart = to_bits(16, start_element); - let elem_offset = start_element * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(result) => write_single_element(load_width_bytes * 8, i, 0, vd + to_bits(5, j) , result), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + vstart = to_bits(16, cur_elem); + let elem_offset = cur_elem * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { + MemValue(result) => write_single_element(load_width_bytes * 8, i, 0, vd + to_bits(5, j) , result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - }; - start_element = start_element + 1 - } - }; + } + }; + cur_elem = cur_elem + 1 + } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VLRETYPE(nf, rs1, width, vd)) = { @@ -1339,83 +1304,79 @@ mapping clause encdec = VSRETYPE(nf, rs1, vs3) if haveRVV() val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { let width_type : word_width = BYTE; - start_element = get_start_element(); - status : Retired = RETIRE_SUCCESS; - if start_element >= nf * elem_per_reg then return status; /* no elements are written */ + 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; - elem_to_align : int = start_element % elem_per_reg; + cur_elem : int = start_element; if elem_to_align > 0 then { foreach (i from elem_to_align to (elem_per_reg - 1)) { - if status != RETIRE_FAIL then { - vstart = to_bits(16, start_element); - let elem_offset : int = start_element * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let one_elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, 0, vs3 + to_bits(5, cur_field)); - let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, one_elem_val, false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + vstart = to_bits(16, cur_elem); + let elem_offset : int = cur_elem * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, 0, vs3 + to_bits(5, cur_field)); + let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - }; - start_element = start_element + 1 - } + } + }; + cur_elem = cur_elem + 1 }; cur_field = cur_field + 1 }; foreach (j from cur_field to (nf - 1)) { - let vs_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, dec, 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)) { - if status != RETIRE_FAIL then { - vstart = to_bits(16, start_element); - let elem_offset = start_element * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs_val[i], false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + vstart = to_bits(16, cur_elem); + let elem_offset = cur_elem * load_width_bytes; + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - }; - start_element = start_element + 1 - } + } + }; + cur_elem = cur_elem + 1 } }; vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VSRETYPE(nf, rs1, vs3)) = { @@ -1445,86 +1406,79 @@ mapping encdec_lsop : vmlsop <-> bits(7) = { mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if haveRVV() <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if haveRVV() -val process_vm : forall 'n 'p, ('n >= 0). (regidx, regidx, int('p), int('n), vmlsop) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} -function process_vm(vd_or_vs3, rs1, EMUL_pow, num_elem, op) = { +val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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, EMUL_pow, vd_or_vs3); - total : vector('n, dec, bits(8)) = undefined; - elem_offset : int = undefined; - status : Retired = RETIRE_SUCCESS; - - foreach (i from 0 to (num_elem - 1)) { - if status != RETIRE_FAIL then { - let elem_offset = i; + let vd_or_vs3_val : vector('n, dec, 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 */ + vstart = to_bits(16, i); if op == VLM then { /* load */ - if i < start_element then { - total[i] = vd_or_vs3_val[i] - } else { - vstart = to_bits(16, i); - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - match mem_read(Read(Data), paddr, 1, false, false, false) { - MemValue(result) => if i < num_elem then total[i] = result, - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, 1, false, false, false) { + MemValue(result) => write_single_element(8, i, 0, vd_or_vs3, result), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } - } - }; + } + } } else if op == VSM then { /* store */ - if i >= start_element then { - vstart = to_bits(16, i); - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); status = RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); status = RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL }, - MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, vd_or_vs3_val[i], false, false, false); - match (res) { - MemValue(true) => status = RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); status = RETIRE_FAIL } - } + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), width_type) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width_type) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, vd_or_vs3_val[i], false, false, false); + match (res) { + MemValue(true) => (), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } } } - } + } } } + } else { /* tail elements for mask load, always with agnostic policy */ + if op == VLM then { + write_single_element(8, i, 0, vd_or_vs3, vd_or_vs3_val[i]) + /* TODO: configuration support for agnostic behavior */ + } } }; - if op == VLM & status == RETIRE_SUCCESS then write_vreg(num_elem, 8, EMUL_pow, vd_or_vs3, total); vstart = EXTZ(0b0); - status + RETIRE_SUCCESS } function clause execute(VMTYPE(rs1, vd_or_vs3, op)) = { let EEW = 8; let EMUL_pow = 0; - let tmp = unsigned(vl); - let num_elem : int = if tmp % 8 == 0 then tmp / 8 else tmp / 8 + 1; + let vl_val = unsigned(vl); + let evl : int = if vl_val % 8 == 0 then vl_val / 8 else vl_val / 8 + 1; /* the effective vector length is evl=ceil(vl/8) */ + let num_elem = get_num_elem(EMUL_pow, EEW); if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; - /* unmask vle8 except that the effective vector length is evl=ceil(vl/8) */ - assert(num_elem >= 0); - process_vm(vd_or_vs3, rs1, EMUL_pow, num_elem, op) + assert(evl >= 0); + process_vm(vd_or_vs3, rs1, num_elem, evl, op) } mapping vmtype_mnemonic : vmlsop <-> string = { diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index afa0b95ea..6118c7dbd 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -55,32 +55,32 @@ mapping clause encdec = RIVVTYPE(funct6, vm, vs2, vs1, vd) if haveRVV() function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; + let num_elem_vs = get_num_elem(LMUL_pow, SEW); + let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ if illegal_reduction_widen(SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; - let 'n = num_elem; + if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ + + let 'n = num_elem_vs; + let 'd = num_elem_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 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; - - assert(8 <= SEW_widen & SEW_widen <= 64); - (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + 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 scalar : bits('o) = read_single_element(SEW_widen, 0, LMUL_pow_widen, vs1); + let scalar : bits('o) = read_single_element(SEW_widen, 0, 0, vs1); /* vs1 regardless of LMUL setting */ sum : bits('o) = match funct6 { IVV_VWREDSUMU => to_bits(SEW_widen, unsigned(scalar)), IVV_VWREDSUM => to_bits(SEW_widen, signed(scalar)) }; - foreach (i from 0 to (num_elem - 1)) { + foreach (i from 0 to (num_elem_vs - 1)) { if mask[i] then { sum = match funct6 { IVV_VWREDSUMU => to_bits(SEW_widen, unsigned(vs2_val[i]) + unsigned(sum)), @@ -89,7 +89,9 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { } }; - write_single_element(SEW_widen, 0, LMUL_pow_widen, vd, sum); + write_single_element(SEW_widen, 0, 0, vd, sum); + /* other elements in vd are treated as tail elements, currently remain unchanged */ + /* TODO: configuration support for agnostic behavior */ vstart = EXTZ(0b0); RETIRE_SUCCESS } @@ -122,23 +124,24 @@ mapping clause encdec = RMVVTYPE(funct6, vm, vs2, vs1, vd) if haveRVV() function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); + let num_elem_vs = get_num_elem(LMUL_pow, SEW); + let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ if illegal_reduction() then { handle_illegal(); return RETIRE_FAIL }; - let 'n = num_elem; - let 'm = SEW; + if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ - 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('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - result : vector('n, dec, bits('m)) = undefined; - mask : vector('n, dec, bool) = undefined; + let 'n = num_elem_vs; + let 'd = num_elem_vd; + let 'm = SEW; - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + 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); - sum : bits('m) = read_single_element(SEW, 0, LMUL_pow, vs1); - foreach (i from 0 to (num_elem - 1)) { + sum : bits('m) = read_single_element(SEW, 0, 0, vs1); /* vs1 regardless of LMUL setting */ + foreach (i from 0 to (num_elem_vs - 1)) { if mask[i] then { sum = match funct6 { MVV_VREDSUM => sum + vs2_val[i], @@ -153,7 +156,9 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { } }; - write_single_element(SEW, 0, LMUL_pow, vd, sum); + write_single_element(SEW, 0, 0, vd, sum); + /* other elements in vd are treated as tail elements, currently remain unchanged */ + /* TODO: configuration support for agnostic behavior */ vstart = EXTZ(0b0); RETIRE_SUCCESS } @@ -188,26 +193,29 @@ mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveRVV() <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveRVV() val process_rfvv_single: forall 'n 'm 'p, 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg} -function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) = { +function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr.FRM(); + let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ + if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); - let 'n = num_elem; - let 'm = SEW; + if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ - 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('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - result : vector('n, dec, bits('m)) = undefined; - mask : vector('n, dec, bool) = undefined; + let 'n = num_elem_vs; + let 'd = num_elem_vd; + let 'm = SEW; - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + 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); - sum : bits('m) = read_single_element(SEW, 0, LMUL_pow, vs1); - foreach (i from 0 to (num_elem - 1)) { + sum : bits('m) = read_single_element(SEW, 0, 0, vs1); /* vs1 regardless of LMUL setting */ + foreach (i from 0 to (num_elem_vs - 1)) { if mask[i] then { sum = match funct6 { + /* currently ordered/unordered sum reductions do the same operations */ FVV_VFREDOSUM => fp_add(rm_3b, sum, vs2_val[i]), FVV_VFREDUSUM => fp_add(rm_3b, sum, vs2_val[i]), FVV_VFREDMAX => fp_max(sum, vs2_val[i]), @@ -216,41 +224,46 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) } }; - write_single_element(SEW, 0, LMUL_pow, vd, sum); + write_single_element(SEW, 0, 0, vd, sum); + /* other elements in vd are treated as tail elements, currently remain unchanged */ + /* TODO: configuration support for agnostic behavior */ vstart = EXTZ(0b0); RETIRE_SUCCESS } val process_rfvv_widen: forall 'n 'm 'p, 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg} -function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) = { +function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr.FRM(); let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; + let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ if illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); - let 'n = num_elem; + if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ + + let 'n = num_elem_vs; + let 'd = num_elem_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 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; - - (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + 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); - sum : bits('o) = read_single_element(SEW_widen, 0, LMUL_pow_widen, vs1); - foreach (i from 0 to (num_elem - 1)) { + sum : bits('o) = read_single_element(SEW_widen, 0, 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 */ + /* currently ordered/unordered sum reductions do the same operations */ sum = fp_add(rm_3b, sum, fp_widen(vs2_val[i])) } }; - write_single_element(SEW_widen, 0, LMUL_pow_widen, vd, sum); + write_single_element(SEW_widen, 0, 0, vd, sum); + /* other elements in vd are treated as tail elements, currently remain unchanged */ + /* TODO: configuration support for agnostic behavior */ vstart = EXTZ(0b0); RETIRE_SUCCESS } @@ -258,12 +271,12 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) = function clause execute(RFVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); + let num_elem_vs = get_num_elem(LMUL_pow, SEW); if funct6 == FVV_VFWREDOSUM | funct6 == FVV_VFWREDUSUM then - process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) + process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) else - process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) + process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) } mapping rfvvtype_mnemonic : rfvvfunct6 <-> string = { diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index d498cbe01..ef0d5b1e2 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -112,6 +112,16 @@ function valid_reg_overlap(rs, rd, EMUL_pow_rs, EMUL_pow_rd) = { is_valid } +/* Check for valid register grouping in vector segment load/store instructions: + * The EMUL of load vd or store vs3 times the number of fields per segment + * must not be larger than 8. (EMUL * NFIELDS <= 8) + */ +val valid_segment : (int, int) -> bool +function valid_segment(nf, EMUL_pow) = { + if EMUL_pow < 0 then nf / int_power(2, 0 - EMUL_pow) <= 8 + else nf * int_power(2, EMUL_pow) <= 8 +} + /* ******************************************************************************* */ /* The following functions summarize patterns of illegal instruction check. */ /* ******************************************************************************* */ @@ -202,6 +212,18 @@ function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = { not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) } +/* m. Normal check for segment load instructions */ +val illegal_segment_load : (regidx, bits(1), int, int) -> bool +function illegal_segment_load(vd, vm, nf, EMUL_pow) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_segment(nf, EMUL_pow)) +} + +/* m. Normal check for segment store instructions (no vd) */ +val illegal_segment_store : (int, int) -> bool +function illegal_segment_store(nf, EMUL_pow) = { + not(valid_vtype()) | not(valid_segment(nf, EMUL_pow)) +} + /* Scalar register shaping */ val get_scalar : forall 'n, 'n >= 8. (regidx, int('n)) -> bits('n) effect {escape, rreg} function get_scalar(rs1, SEW) = { @@ -246,7 +268,7 @@ function get_end_element() = { * 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, 8 <= 'm <= 64. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) effect {escape, rreg, undef, wreg} +val init_masked_result : forall 'n 'm 'p. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) effect {escape, rreg, undef} 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(); @@ -256,7 +278,7 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { 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 / (0 - LMUL_pow); + let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / int_power(2, 0 - LMUL_pow); assert(num_elem >= real_num_elem); foreach (i from 0 to (num_elem - 1)) { @@ -297,9 +319,46 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { (result, mask) } +/* For instructions like vector reduction and vector store, + * masks on prestart, inactive and tail elements only affect the validation of source register elements + * (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. (int('n), int('p), vector('n, dec, bool)) -> vector('n, dec, bool) effect {escape, rreg, undef} +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; + + /* Determine the actual number of elements when lmul < 1 */ + let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / int_power(2, 0 - LMUL_pow); + assert(num_elem >= real_num_elem); + + foreach (i from 0 to (num_elem - 1)) { + if i < start_element then { + /* Prestart elements defined by vstart */ + mask[i] = false + } else if i > end_element then { + /* Tail elements defined by vl */ + mask[i] = false + } else if i >= real_num_elem then { + /* Tail elements defined by lmul < 1 */ + mask[i] = false + } else if not(vm_val[i]) then { + /* Inactive body elements defined by vm */ + mask[i] = false + } else { + /* Active body elements */ + mask[i] = true; + } + }; + + mask +} + /* 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, 8 <= 'm <= 64. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef, wreg} +val init_masked_result_carry : forall 'n 'm 'p. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef} function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { let start_element = get_start_element(); let end_element = get_end_element(); @@ -307,7 +366,7 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { 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 / (0 - LMUL_pow); + let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / int_power(2, 0 - LMUL_pow); assert(num_elem >= real_num_elem); foreach (i from 0 to (num_elem - 1)) { @@ -335,7 +394,7 @@ 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, 8 <= 'm <= 64. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef, wreg} +val init_masked_result_cmp : forall 'n 'm 'p. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef} 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(); @@ -344,7 +403,7 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { 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 / (0 - LMUL_pow); + let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / int_power(2, 0 - LMUL_pow); assert(num_elem >= real_num_elem); foreach (i from 0 to (num_elem - 1)) { @@ -379,6 +438,28 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { (result, mask) } +/* For vector load/store segment instructions: + * 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. (int('n), int('m), int('p), int('q), regidx) -> vector('n, dec, bits('q * 'm)) effect {escape, rreg, undef} +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 int_power(2, LMUL_pow); + vreg_list : vector('q, dec, vector('n, dec, bits('m))) = undefined; + 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)); + }; + foreach (i from 0 to (num_elem - 1)) { + result[i] = zeros('q * 'm); + foreach (j from 0 to (nf - 1)) { + result[i] = result[i] | EXTZ(vreg_list[j][i] << (j * 'm)) + } + }; + result +} + /* Floating point canonical NaN for 16-bit, 32-bit, 64-bit and 128-bit types */ val canonical_NaN : forall 'm, 'm in {16, 32, 64, 128}. int('m) -> bits('m) function canonical_NaN('m) = { diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index d84adc62d..2ae1854b3 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -45,12 +45,8 @@ mapping sew_flag : string <-> bits(3) = { "e8" <-> 0b000, "e16" <-> 0b001, "e32" <-> 0b010, - "e64" <-> 0b011, - "e128" <-> 0b100, - "e256" <-> 0b101, - "e512" <-> 0b110, - "e1024" <-> 0b111 -} + "e64" <-> 0b011 +} mapping maybe_lmul_flag : string <-> bits(3) = { "" <-> 0b000, /* m1 by default */ diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index bbd52868c..cd85ff737 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -292,38 +292,6 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { V(vrid) = r } -/* Reads multiple vregs into a single element */ -val read_mult_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx) -> bits('m) effect {escape, rreg} -function read_mult_vreg(num_vreg, SEW, vrid) = { - let VLEN = int_power(2, get_vlen_pow()); - assert(0 < VLEN & VLEN <= sizeof(vlenmax)); - assert('m >= VLEN); - var result : bits('m) = zeros(); - - foreach (i from (num_vreg - 1) downto 0) { - let vrid_lmul : regidx = vrid + to_bits(5, i); - let bv : vregtype = V(vrid_lmul); - - result = (result << VLEN); - result = result | sail_zero_extend(bv[VLEN - 1 .. 0], SEW); - }; - - result -} - -/* Writes a single element into multiple vregs */ -val write_mult_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx, bits('m)) -> unit effect {escape, rreg, wreg} -function write_mult_vreg(num_vreg, SEW, vrid, bv) = { - let VLEN = int_power(2, get_vlen_pow()); - assert(0 < VLEN & VLEN <= sizeof(vlenmax)); - assert('m >= VLEN); - foreach (i from (num_vreg - 1) downto 0) { - let vrid_lmul : regidx = vrid + to_bits(5, i); - let single_bv : vregtype = sail_zero_extend(slice(bv >> (VLEN * i), 0, VLEN), sizeof(vlenmax)); - V(vrid_lmul) = single_bv - } -} - /* The general vreg reading operation with num_elem as max(VLMAX,VLEN/SEW)) */ val read_vreg : forall 'n 'm 'p. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef} function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { @@ -334,35 +302,25 @@ function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { /* Check for valid vrid */ if unsigned(vrid) + 2 ^ LMUL_pow_reg > 32 then { /* vrid would read past largest vreg (v31) */ - result = undefined + assert(false, "invalid register group: vrid overflow the largest number") } else if unsigned(vrid) % (2 ^ LMUL_pow_reg) != 0 then { - /* vrid must be a multiple of lmul */ - result = undefined + /* vrid must be a multiple of emul */ + assert(false, "invalid register group: vrid is not a multiple of EMUL") } else { - if SEW > VLEN then { - /* Multiple vregs per element */ - let 'num_reg_per_elem : int = SEW / VLEN; - assert('num_reg_per_elem >= 0); - foreach (i from 0 to (num_elem - 1)) { - let vrid_lmul : regidx = vrid + to_bits(5, i * 'num_reg_per_elem); - result[i] = read_mult_vreg('num_reg_per_elem, SEW, vrid_lmul) - } + if LMUL_pow < 0 then { + result = read_single_vreg('n, SEW, vrid); } else { - if LMUL_pow < 0 then { - result = read_single_vreg('n, SEW, vrid); - } else { - let 'num_elem_single : int = VLEN / SEW; - foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) { - 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); - 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); - assert(0 <= s_i & s_i < 'num_elem_single); - result[r_i] = single_result[s_i]; - } + let 'num_elem_single : int = VLEN / SEW; + foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) { + 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); + 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); + assert(0 <= s_i & s_i < 'num_elem_single); + result[r_i] = single_result[s_i]; } } } @@ -390,29 +348,19 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { let VLEN = int_power(2, get_vlen_pow()); let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; - if SEW > VLEN then { - /* Multiple vregs per element */ - let 'num_reg_per_elem : int = SEW / VLEN; - assert('num_reg_per_elem >= 0); - foreach (i from 0 to (num_elem - 1)) { - let vrid_lmul : regidx = vrid + to_bits(5, i * 'num_reg_per_elem); - write_mult_vreg('num_reg_per_elem, SEW, vrid_lmul, vec[i]) - } - } else { - let 'num_elem_single : int = VLEN / SEW; - foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) { - var single_vec : vector('num_elem_single, dec, bits('m)) = undefined; - 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; - 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); - assert(0 <= s_i & s_i < 'num_elem_single); - single_vec[s_i] = vec[r_i] - }; - write_single_vreg('num_elem_single, SEW, vrid_lmul, single_vec) - } + let 'num_elem_single : int = VLEN / SEW; + foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) { + var single_vec : vector('num_elem_single, dec, bits('m)) = undefined; + 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; + 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); + assert(0 <= s_i & s_i < 'num_elem_single); + single_vec[s_i] = vec[r_i] + }; + write_single_vreg('num_elem_single, SEW, vrid_lmul, single_vec) } } diff --git a/model/riscv_vlen.sail b/model/riscv_vlen.sail index f8ba1f46c..55f18eac5 100644 --- a/model/riscv_vlen.sail +++ b/model/riscv_vlen.sail @@ -74,4 +74,7 @@ type vlenmax : Int = 65536 * means VLEN = 1024 and ELEN = 64, * and the CSR vlenb is also not used. * They will be configurable when user-specified configuration is supported in Sail. + * + * Also, VLEN >= ELEN must be satisfied and this condition check should be added + * after their initialization. */