From 9d86f01584f7e9ff2958c8ee9ffc9b65151c235f Mon Sep 17 00:00:00 2001 From: guan jian <148229859+rez5427@users.noreply.github.com> Date: Tue, 29 Oct 2024 16:53:41 +0800 Subject: [PATCH] Remove vlenb register Remove `vlenb` register which does not have any mutable state. Co-authored-by: Yui5427 <785369607@qq.com> --- model/riscv_insts_vext_mask.sail | 12 ++++++------ model/riscv_insts_vext_mem.sail | 2 -- model/riscv_sys_control.sail | 4 ---- model/riscv_sys_regs.sail | 5 ++++- model/riscv_vext_control.sail | 5 +---- model/riscv_vext_regs.sail | 7 ------- model/riscv_vlen.sail | 2 ++ 7 files changed, 13 insertions(+), 24 deletions(-) diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index e4e29a77b..ae30bc114 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -31,7 +31,7 @@ mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = VLEN; if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; @@ -88,7 +88,7 @@ mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V) function clause execute(VCPOP_M(vm, vs2, rd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = VLEN; if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; @@ -122,7 +122,7 @@ mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V) function clause execute(VFIRST_M(vm, vs2, rd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = VLEN; if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; @@ -158,7 +158,7 @@ mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSBF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = VLEN; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; @@ -198,7 +198,7 @@ mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSIF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = VLEN; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; @@ -238,7 +238,7 @@ mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSOF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = VLEN; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index cc8161304..41c235abd 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -694,7 +694,6 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { function clause execute(VLRETYPE(nf, rs1, width, vd)) = { let load_width_bytes = vlewidth_bytesnumber(width); let EEW = load_width_bytes * 8; - let VLEN = unsigned(vlenb) * 8; let elem_per_reg : int = VLEN / EEW; let nf_int = nfields_int(nf); @@ -794,7 +793,6 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { function clause execute(VSRETYPE(nf, rs1, vs3)) = { let load_width_bytes = 1; let EEW = 8; - let VLEN = unsigned(vlenb) * 8; let elem_per_reg : int = VLEN / EEW; let nf_int = nfields_int(nf); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 620240cb9..6379f5676 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -470,10 +470,6 @@ function init_sys() -> unit = { menvcfg.bits = zeros(); senvcfg.bits = zeros(); /* initialize vector csrs */ - vlenb = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */ - /* VLEN value needs to be manually changed currently. - * See riscv_vlen.sail for details. - */ vstart = zeros(); vl = zeros(); vcsr[vxrm] = 0b00; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 8bbf68e75..e7ca84887 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -799,7 +799,10 @@ function is_fiom_active() -> bool = { /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vl : xlenbits -register vlenb : xlenbits + +function get_vlenb() -> xlenbits = { + to_bits(xlen, (2 ^ (get_vlen_pow()) / 8)) +} bitfield Vtype : xlenbits = { vill : xlen - 1, diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 3dabc1fc0..167b44a1c 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -20,12 +20,9 @@ function clause read_CSR(0x00A) = zero_extend(vcsr[vxrm]) function clause read_CSR(0x00F) = zero_extend(vcsr.bits) function clause read_CSR(0xC20) = vl function clause read_CSR(0xC21) = vtype.bits -function clause read_CSR(0xC22) = vlenb +function clause read_CSR(0xC22) = get_vlenb() function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) } function clause write_CSR(0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) } function clause write_CSR(0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); zero_extend(vcsr[vxrm]) } function clause write_CSR(0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) } -function clause write_CSR(0xC20, value) = { vl = value; vl } -function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits } -function clause write_CSR(0xC22, value) = { vlenb = value; vlenb } diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index aadd05bc2..6b1b98dd4 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -161,7 +161,6 @@ function wV (r : regno, v : vregtype) -> unit = { dirty_v_context(); - let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); if get_config_print_reg() then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0])); @@ -229,7 +228,6 @@ function ext_write_vcsr (vxrm_val, vxsat_val) = { /* num_elem means max(VLMAX,VLEN/SEW)) according to Section 5.4 of RVV spec */ val get_num_elem : (int, int) -> nat function get_num_elem(LMUL_pow, SEW) = { - let VLEN = unsigned(vlenb) * 8; 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 */ @@ -271,7 +269,6 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, bits('m)) function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { var result : vector('n, bits('m)) = vector_init(zeros()); - let VLEN = unsigned(vlenb) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; /* Check for valid vrid */ @@ -308,7 +305,6 @@ function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { /* Single element reading operation */ val read_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx) -> bits('m) function read_single_element(EEW, index, vrid) = { - let VLEN = unsigned(vlenb) * 8; assert(VLEN >= EEW); let 'elem_per_reg : int = VLEN / EEW; assert('elem_per_reg >= 0); @@ -322,7 +318,6 @@ function read_single_element(EEW, index, vrid) = { /* The general vreg writing operation with num_elem as max(VLMAX,VLEN/SEW)) */ val write_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, bits('m))) -> unit function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { - let VLEN = unsigned(vlenb) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; let 'num_elem_single : int = VLEN / SEW; @@ -345,7 +340,6 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { /* Single element writing operation */ val write_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx, bits('m)) -> unit function write_single_element(EEW, index, vrid, value) = { - let VLEN = unsigned(vlenb) * 8; let 'elem_per_reg : int = VLEN / EEW; assert('elem_per_reg >= 0); let real_vrid : regidx = vrid + to_bits(5, index / 'elem_per_reg); @@ -403,7 +397,6 @@ function read_vmask_carry(num_elem, vm, vrid) = { /* Mask register writing operation with num_elem as max(VLMAX,VLEN/SEW)) */ val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, bool)) -> unit function write_vmask(num_elem, vrid, v) = { - let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); assert(0 < num_elem & num_elem <= VLEN); let vreg_val : vregtype = V(vrid); diff --git a/model/riscv_vlen.sail b/model/riscv_vlen.sail index d3c741780..33a529237 100644 --- a/model/riscv_vlen.sail +++ b/model/riscv_vlen.sail @@ -20,3 +20,5 @@ val sys_vector_vlen_exp = pure "sys_vector_vlen_exp" : unit -> range(3, 16) function get_vlen_pow() -> range(3, 16) = sys_vector_vlen_exp() type vlenmax : Int = 65536 + +let VLEN = 2 ^ get_vlen_pow()