diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 41c235abd..febded099 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -69,7 +69,7 @@ mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ex val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); @@ -135,7 +135,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled( val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); @@ -240,7 +240,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); @@ -309,7 +309,7 @@ mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnab val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); @@ -376,7 +376,7 @@ mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEna val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); @@ -446,7 +446,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { - let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); + let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow; let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); @@ -538,7 +538,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { - let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); + let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow; let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index ce2f1995a..d5833f162 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -60,8 +60,8 @@ function valid_rd_mask(rd, vm) = { */ val valid_reg_overlap : (regidx, regidx, int, int) -> bool function valid_reg_overlap(rs, rd, EMUL_pow_rs, EMUL_pow_rd) = { - let rs_group = if EMUL_pow_rs > 0 then 2 ^ (EMUL_pow_rs) else 1; - let rd_group = if EMUL_pow_rd > 0 then 2 ^ (EMUL_pow_rd) else 1; + let rs_group = if EMUL_pow_rs > 0 then 2 ^ EMUL_pow_rs else 1; + let rd_group = if EMUL_pow_rd > 0 then 2 ^ EMUL_pow_rd else 1; let rs_int = unsigned(rs); let rd_int = unsigned(rd); if EMUL_pow_rs < EMUL_pow_rd then { @@ -79,7 +79,7 @@ function valid_reg_overlap(rs, rd, EMUL_pow_rs, EMUL_pow_rd) = { val valid_segment : (int, int) -> bool function valid_segment(nf, EMUL_pow) = { if EMUL_pow < 0 then nf / (2 ^ (0 - EMUL_pow)) <= 8 - else nf * 2 ^ (EMUL_pow) <= 8 + else nf * 2 ^ EMUL_pow <= 8 } /* ******************************************************************************* */ @@ -371,7 +371,7 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { */ val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'm >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, bits('q * 'm)) function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { - let LMUL_reg : int = if LMUL_pow <= 0 then 1 else 2 ^ (LMUL_pow); + let LMUL_reg : int = if LMUL_pow <= 0 then 1 else 2 ^ LMUL_pow; var vreg_list : vector('q, vector('n, bits('m))) = vector_init(vector_init(zeros())); var result : vector('n, bits('q * 'm)) = vector_init(zeros()); foreach (j from 0 to (nf - 1)) { diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 14947e77c..2c913de83 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -227,7 +227,7 @@ function get_num_elem(LMUL_pow, SEW) = { let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; /* Ignore lmul < 1 so that the entire vreg is read, allowing all masking to * be handled in init_masked_result */ - let num_elem = 2 ^ (LMUL_pow_reg) * VLEN / SEW; + let num_elem = 2 ^ LMUL_pow_reg * VLEN / SEW; assert(num_elem > 0); num_elem }