Skip to content

Commit c031994

Browse files
Yui5427Yui5427
committed
remove register vlenb
1 parent 9be19c6 commit c031994

7 files changed

+47
-22
lines changed

‎model/riscv_insts_vext_mask.sail

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V)
3131
function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
3232
let SEW = get_sew();
3333
let LMUL_pow = get_lmul_pow();
34-
let num_elem = unsigned(vlenb) * 8;
34+
let num_elem = unsigned(get_vlenb()) * 8;
3535

3636
if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL };
3737

@@ -88,7 +88,7 @@ mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V)
8888
function clause execute(VCPOP_M(vm, vs2, rd)) = {
8989
let SEW = get_sew();
9090
let LMUL_pow = get_lmul_pow();
91-
let num_elem = unsigned(vlenb) * 8;
91+
let num_elem = unsigned(get_vlenb()) * 8;
9292

9393
if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL };
9494

@@ -122,7 +122,7 @@ mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V)
122122
function clause execute(VFIRST_M(vm, vs2, rd)) = {
123123
let SEW = get_sew();
124124
let LMUL_pow = get_lmul_pow();
125-
let num_elem = unsigned(vlenb) * 8;
125+
let num_elem = unsigned(get_vlenb()) * 8;
126126

127127
if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL };
128128

@@ -158,7 +158,7 @@ mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
158158
function clause execute(VMSBF_M(vm, vs2, vd)) = {
159159
let SEW = get_sew();
160160
let LMUL_pow = get_lmul_pow();
161-
let num_elem = unsigned(vlenb) * 8;
161+
let num_elem = unsigned(get_vlenb()) * 8;
162162

163163
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
164164
then { handle_illegal(); return RETIRE_FAIL };
@@ -198,7 +198,7 @@ mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
198198
function clause execute(VMSIF_M(vm, vs2, vd)) = {
199199
let SEW = get_sew();
200200
let LMUL_pow = get_lmul_pow();
201-
let num_elem = unsigned(vlenb) * 8;
201+
let num_elem = unsigned(get_vlenb()) * 8;
202202

203203
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
204204
then { handle_illegal(); return RETIRE_FAIL };
@@ -238,7 +238,7 @@ mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
238238
function clause execute(VMSOF_M(vm, vs2, vd)) = {
239239
let SEW = get_sew();
240240
let LMUL_pow = get_lmul_pow();
241-
let num_elem = unsigned(vlenb) * 8;
241+
let num_elem = unsigned(get_vlenb()) * 8;
242242

243243
if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
244244
then { handle_illegal(); return RETIRE_FAIL };

‎model/riscv_insts_vext_mem.sail

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -694,7 +694,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
694694
function clause execute(VLRETYPE(nf, rs1, width, vd)) = {
695695
let load_width_bytes = vlewidth_bytesnumber(width);
696696
let EEW = load_width_bytes * 8;
697-
let VLEN = unsigned(vlenb) * 8;
697+
let VLEN = unsigned(get_vlenb()) * 8;
698698
let elem_per_reg : int = VLEN / EEW;
699699
let nf_int = nfields_int(nf);
700700

@@ -794,7 +794,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
794794
function clause execute(VSRETYPE(nf, rs1, vs3)) = {
795795
let load_width_bytes = 1;
796796
let EEW = 8;
797-
let VLEN = unsigned(vlenb) * 8;
797+
let VLEN = unsigned(get_vlenb()) * 8;
798798
let elem_per_reg : int = VLEN / EEW;
799799
let nf_int = nfields_int(nf);
800800

‎model/riscv_insts_zcmp.sail

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
/*=======================================================================================*/
2+
/* This Sail RISC-V architecture model, comprising all files and */
3+
/* directories except where otherwise noted is subject the BSD */
4+
/* two-clause license in the LICENSE file. */
5+
/* */
6+
/* SPDX-License-Identifier: BSD-2-Clause */
7+
/*=======================================================================================*/
8+
9+
enum clause extension = Ext_Zcmp
10+
function clause extensionEnabled(Ext_Zcmp) = sys_enable_zcb()
11+
12+
union clause ast = C_LBU : (bits(2), cregidx, cregidx)
13+
14+
mapping clause encdec_compressed =
15+
C_LBU(uimm1 @ uimm0, rdc, rs1c) if extensionEnabled(Ext_Zcmp)
16+
<-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_Zcmp)
17+
18+
mapping clause assembly = C_LBU(uimm, rdc, rs1c) <->
19+
"c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
20+
21+
function clause execute C_LBU(uimm, rdc, rs1c) = {
22+
let imm : bits(12) = zero_extend(uimm);
23+
let rd = creg2reg_idx(rdc);
24+
let rs1 = creg2reg_idx(rs1c);
25+
execute(LOAD(imm, rs1, rd, true, BYTE, false, false))
26+
}

‎model/riscv_sys_control.sail

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -470,10 +470,7 @@ function init_sys() -> unit = {
470470
menvcfg.bits = zeros();
471471
senvcfg.bits = zeros();
472472
/* initialize vector csrs */
473-
vlenb = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */
474-
/* VLEN value needs to be manually changed currently.
475-
* See riscv_vlen.sail for details.
476-
*/
473+
477474
vstart = zeros();
478475
vl = zeros();
479476
vcsr[vxrm] = 0b00;

‎model/riscv_sys_regs.sail

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -799,7 +799,10 @@ function is_fiom_active() -> bool = {
799799
/* vector csrs */
800800
register vstart : bits(16) /* use the largest possible length of vstart */
801801
register vl : xlenbits
802-
register vlenb : xlenbits
802+
803+
function get_vlenb() -> xlenbits = {
804+
to_bits(xlen, (2 ^ (get_vlen_pow()) / 8))
805+
}
803806

804807
bitfield Vtype : xlenbits = {
805808
vill : xlen - 1,

‎model/riscv_vext_control.sail

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,11 @@ function clause read_CSR(0x00A) = zero_extend(vcsr[vxrm])
2020
function clause read_CSR(0x00F) = zero_extend(vcsr.bits)
2121
function clause read_CSR(0xC20) = vl
2222
function clause read_CSR(0xC21) = vtype.bits
23-
function clause read_CSR(0xC22) = vlenb
23+
function clause read_CSR(0xC22) = get_vlenb()
2424

2525
function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) }
2626
function clause write_CSR(0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) }
2727
function clause write_CSR(0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); zero_extend(vcsr[vxrm]) }
2828
function clause write_CSR(0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) }
2929
function clause write_CSR(0xC20, value) = { vl = value; vl }
3030
function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits }
31-
function clause write_CSR(0xC22, value) = { vlenb = value; vlenb }

‎model/riscv_vext_regs.sail

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ function wV (r : regno, v : vregtype) -> unit = {
161161

162162
dirty_v_context();
163163

164-
let VLEN = unsigned(vlenb) * 8;
164+
let VLEN = unsigned(get_vlenb()) * 8;
165165
assert(0 < VLEN & VLEN <= sizeof(vlenmax));
166166
if get_config_print_reg()
167167
then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
@@ -229,7 +229,7 @@ function ext_write_vcsr (vxrm_val, vxsat_val) = {
229229
/* num_elem means max(VLMAX,VLEN/SEW)) according to Section 5.4 of RVV spec */
230230
val get_num_elem : (int, int) -> nat
231231
function get_num_elem(LMUL_pow, SEW) = {
232-
let VLEN = unsigned(vlenb) * 8;
232+
let VLEN = unsigned(get_vlenb()) * 8;
233233
let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
234234
/* Ignore lmul < 1 so that the entire vreg is read, allowing all masking to
235235
* be handled in init_masked_result */
@@ -271,7 +271,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = {
271271
val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, bits('m))
272272
function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
273273
var result : vector('n, bits('m)) = vector_init(zeros());
274-
let VLEN = unsigned(vlenb) * 8;
274+
let VLEN = unsigned(get_vlenb()) * 8;
275275
let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
276276

277277
/* Check for valid vrid */
@@ -308,7 +308,7 @@ function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
308308
/* Single element reading operation */
309309
val read_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx) -> bits('m)
310310
function read_single_element(EEW, index, vrid) = {
311-
let VLEN = unsigned(vlenb) * 8;
311+
let VLEN = unsigned(get_vlenb()) * 8;
312312
assert(VLEN >= EEW);
313313
let 'elem_per_reg : int = VLEN / EEW;
314314
assert('elem_per_reg >= 0);
@@ -322,7 +322,7 @@ function read_single_element(EEW, index, vrid) = {
322322
/* The general vreg writing operation with num_elem as max(VLMAX,VLEN/SEW)) */
323323
val write_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, bits('m))) -> unit
324324
function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
325-
let VLEN = unsigned(vlenb) * 8;
325+
let VLEN = unsigned(get_vlenb()) * 8;
326326
let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
327327

328328
let 'num_elem_single : int = VLEN / SEW;
@@ -345,7 +345,7 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
345345
/* Single element writing operation */
346346
val write_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx, bits('m)) -> unit
347347
function write_single_element(EEW, index, vrid, value) = {
348-
let VLEN = unsigned(vlenb) * 8;
348+
let VLEN = unsigned(get_vlenb()) * 8;
349349
let 'elem_per_reg : int = VLEN / EEW;
350350
assert('elem_per_reg >= 0);
351351
let real_vrid : regidx = vrid + to_bits(5, index / 'elem_per_reg);
@@ -403,7 +403,7 @@ function read_vmask_carry(num_elem, vm, vrid) = {
403403
/* Mask register writing operation with num_elem as max(VLMAX,VLEN/SEW)) */
404404
val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, bool)) -> unit
405405
function write_vmask(num_elem, vrid, v) = {
406-
let VLEN = unsigned(vlenb) * 8;
406+
let VLEN = unsigned(get_vlenb()) * 8;
407407
assert(0 < VLEN & VLEN <= sizeof(vlenmax));
408408
assert(0 < num_elem & num_elem <= VLEN);
409409
let vreg_val : vregtype = V(vrid);

0 commit comments

Comments
 (0)