Skip to content

Commit

Permalink
Remove vlenb register
Browse files Browse the repository at this point in the history 
Remove `vlenb` register which does not have any mutable state. 

Co-authored-by: Yui5427 <[email protected]>
  • Loading branch information
@rez5427 @Yui5427
rez5427 and Yui5427 authored Oct 29, 2024
1 parent 1559013 commit 9d86f01
Show file tree
Hide file tree
Showing 7 changed files with 13 additions and 24 deletions.
12 changes: 6 additions & 6 deletions model/riscv_insts_vext_mask.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 };

Expand Down Expand Up @@ -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 };

Expand Down Expand Up @@ -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 };

Expand Down Expand Up @@ -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 };
Expand Down Expand Up @@ -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 };
Expand Down Expand Up @@ -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 };
Expand Down
2 changes: 0 additions & 2 deletions model/riscv_insts_vext_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down Expand Up @@ -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);

Expand Down
4 changes: 0 additions & 4 deletions model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
5 changes: 4 additions & 1 deletion model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
5 changes: 1 addition & 4 deletions model/riscv_vext_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
7 changes: 0 additions & 7 deletions model/riscv_vext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]));
Expand Down Expand Up @@ -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 */
Expand Down Expand Up @@ -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 */
Expand Down Expand Up @@ -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);
Expand All @@ -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;
Expand All @@ -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);
Expand Down Expand Up @@ -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);
Expand Down
2 changes: 2 additions & 0 deletions model/riscv_vlen.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()

0 comments on commit 9d86f01

Please sign in to comment.