Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove vlenb register #607

Merged
merged 12 commits into from
Oct 29, 2024
12 changes: 6 additions & 6 deletions model/riscv_insts_vext_mask.sail
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 = unsigned(get_vlenb()) * 8;
rez5427 marked this conversation as resolved.
Show resolved Hide resolved

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 = unsigned(get_vlenb()) * 8;

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 = unsigned(get_vlenb()) * 8;

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 = unsigned(get_vlenb()) * 8;

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 = unsigned(get_vlenb()) * 8;

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 = unsigned(get_vlenb()) * 8;

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
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
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
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
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
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
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()
Loading