Skip to content

Commit

Permalink
Rename EXTZ and EXTS in the V extension code
Browse files Browse the repository at this point in the history
  • Loading branch information
@XinlaiWan
XinlaiWan committed Aug 22, 2023
1 parent 8126c2e commit d49437c
Show file tree
Hide file tree
Showing 10 changed files with 126 additions and 125 deletions.
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ bool rv_enable_rvc = true;
bool rv_enable_next = false;
bool rv_enable_writable_misa = true;
bool rv_enable_fdext = true;
bool rv_enable_rvv = true;

bool rv_enable_dirty_update = false;
bool rv_enable_misaligned = false;
Expand Down
142 changes: 71 additions & 71 deletions model/riscv_insts_vext_arith.sail
View file

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions model/riscv_insts_vext_fp.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -436,7 +436,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
},
FV_CVT_F_XU => {
let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
16 => riscv_ui32ToF16(rm_3b, EXTZ(vs2_val[i])),
16 => riscv_ui32ToF16(rm_3b, zero_extend(vs2_val[i])),
32 => riscv_ui32ToF32(rm_3b, vs2_val[i]),
64 => riscv_ui64ToF64(rm_3b, vs2_val[i])
};
Expand All @@ -445,7 +445,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
},
FV_CVT_F_X => {
let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
16 => riscv_i32ToF16(rm_3b, EXTS(vs2_val[i])),
16 => riscv_i32ToF16(rm_3b, sign_extend(vs2_val[i])),
32 => riscv_i32ToF32(rm_3b, vs2_val[i]),
64 => riscv_i64ToF64(rm_3b, vs2_val[i])
};
Expand Down Expand Up @@ -555,17 +555,17 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = {
},
FWV_CVT_F_XU => {
let (fflags, elem) : (bits_fflags, bits('o)) = match 'm {
8 => riscv_ui32ToF16(rm_3b, EXTZ(vs2_val[i])),
16 => riscv_ui32ToF32(rm_3b, EXTZ(vs2_val[i])),
8 => riscv_ui32ToF16(rm_3b, zero_extend(vs2_val[i])),
16 => riscv_ui32ToF32(rm_3b, zero_extend(vs2_val[i])),
32 => riscv_ui32ToF64(rm_3b, vs2_val[i])
};
write_fflags(fflags);
elem
},
FWV_CVT_F_X => {
let (fflags, elem) : (bits_fflags, bits('o)) = match 'm {
8 => riscv_i32ToF16(rm_3b, EXTS(vs2_val[i])),
16 => riscv_i32ToF32(rm_3b, EXTS(vs2_val[i])),
8 => riscv_i32ToF16(rm_3b, sign_extend(vs2_val[i])),
16 => riscv_i32ToF32(rm_3b, sign_extend(vs2_val[i])),
32 => riscv_i32ToF64(rm_3b, vs2_val[i])
};
write_fflags(fflags);
Expand Down
30 changes: 15 additions & 15 deletions model/riscv_insts_vext_utils.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ function get_scalar(rs1, SEW) = {
X(rs1)[SEW - 1 .. 0]
} else {
/* Sign extend to SEW */
EXTS(SEW, X(rs1))
sign_extend(SEW, X(rs1))
}
}

Expand Down Expand Up @@ -462,7 +462,7 @@ function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = {
foreach (i from 0 to (num_elem - 1)) {
result[i] = zeros('q * 'm);
foreach (j from 0 to (nf - 1)) {
result[i] = result[i] | (EXTZ(vreg_list[j][i]) << (j * 'm))
result[i] = result[i] | (zero_extend(vreg_list[j][i]) << (j * 'm))
}
};
result
Expand Down Expand Up @@ -878,7 +878,7 @@ function fp_class(xf) = {
else if f_is_QNaN (xf) then 0b_10_0000_0000
else zeros();

EXTZ(result_val_10b)
zero_extend(result_val_10b)
}

val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) effect {escape, rreg, undef, wreg}
Expand Down Expand Up @@ -951,9 +951,9 @@ function count_leadingzeros (sig, len) = {
val rsqrt7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bool) -> bits_D
function rsqrt7 (v, sub) = {
let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm {
16 => (EXTZ(64, v[9 .. 0]), EXTZ(64, v[14 .. 10]), [v[15]], 5, 10),
32 => (EXTZ(64, v[22 .. 0]), EXTZ(64, v[30 .. 23]), [v[31]], 8, 23),
64 => (EXTZ(64, v[51 .. 0]), EXTZ(64, v[62 .. 52]), [v[63]], 11, 52)
16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10),
32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23),
64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52)
};
assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11);
let table : vector(128, dec, int) = [
Expand All @@ -978,7 +978,7 @@ function rsqrt7 (v, sub) = {
if sub then {
let nr_leadingzeros = count_leadingzeros(sig, s);
assert(nr_leadingzeros >= 0);
(to_bits(64, (0 - nr_leadingzeros)), EXTZ(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros)))
(to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros)))
} else {
(exp, sig)
};
Expand All @@ -991,7 +991,7 @@ function rsqrt7 (v, sub) = {
assert(idx >= 0 & idx < 128);
let out_sig = to_bits(s, table[(127 - idx)]) << (s - 7);
let out_exp = to_bits(e, (3 * (2^(e - 1) - 1) - 1 - signed(normalized_exp)) / 2);
EXTZ(64, sign @ out_exp @ out_sig)
zero_extend(64, sign @ out_exp @ out_sig)
}

val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}
Expand Down Expand Up @@ -1051,9 +1051,9 @@ function riscv_f64Rsqrte7 (rm, v) = {
val recip7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bits(3), bool) -> (bool, bits_D)
function recip7 (v, rm_3b, sub) = {
let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm {
16 => (EXTZ(64, v[9 .. 0]), EXTZ(64, v[14 .. 10]), [v[15]], 5, 10),
32 => (EXTZ(64, v[22 .. 0]), EXTZ(64, v[30 .. 23]), [v[31]], 8, 23),
64 => (EXTZ(64, v[51 .. 0]), EXTZ(64, v[62 .. 52]), [v[63]], 11, 52)
16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10),
32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23),
64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52)
};
assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11);
let table : vector(128, dec, int) = [
Expand All @@ -1078,7 +1078,7 @@ function recip7 (v, rm_3b, sub) = {
assert(nr_leadingzeros >= 0);
let (normalized_exp, normalized_sig) =
if sub then {
(to_bits(64, (0 - nr_leadingzeros)), EXTZ(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros)))
(to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros)))
} else {
(exp, sig)
};
Expand All @@ -1101,10 +1101,10 @@ function recip7 (v, rm_3b, sub) = {

if sub & nr_leadingzeros > 1 then {
if (rm_3b == 0b001 | rm_3b == 0b010 & sign == 0b0 | rm_3b == 0b011 & sign == 0b1) then {
(true, EXTZ(64, sign @ ones(e - 1) @ 0b0 @ ones(s)))
(true, zero_extend(64, sign @ ones(e - 1) @ 0b0 @ ones(s)))
}
else (true, EXTZ(64, sign @ ones(e) @ zeros(s)))
} else (false, EXTZ(64, sign @ out_exp @ out_sig))
else (true, zero_extend(64, sign @ ones(e) @ zeros(s)))
} else (false, zero_extend(64, sign @ out_exp @ out_sig))
}

val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_vext_vm.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -547,7 +547,7 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = {
let 'm = SEW;

let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000);
let imm_val : bits('m) = EXTS(simm);
let imm_val : bits('m) = sign_extend(simm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
Expand Down Expand Up @@ -599,7 +599,7 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let imm_val : bits('m) = EXTS(simm);
let imm_val : bits('m) = sign_extend(simm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
Expand Down Expand Up @@ -658,7 +658,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
};

let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000);
let imm_val : bits('m) = EXTS(simm);
let imm_val : bits('m) = sign_extend(simm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
result : vector('n, dec, bits('m)) = undefined;
Expand Down Expand Up @@ -713,7 +713,7 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = {
let 'm = SEW;

let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let imm_val : bits('m) = EXTS(simm);
let imm_val : bits('m) = sign_extend(simm);
let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
result : vector('n, dec, bool) = undefined;
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_vext_vset.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
let SEW_pow_new = get_sew_pow();
if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
vl = EXTZ(0b0);
vl = zeros();
print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
print_reg("CSR vl <- " ^ BitStr(vl));
return RETIRE_SUCCESS
Expand All @@ -129,7 +129,7 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
let ratio_pow_new = SEW_pow_new - LMUL_pow_new;
if (ratio_pow_new != ratio_pow_ori) then {
vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
vl = EXTZ(0b0);
vl = zeros();
}
};
print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
Expand Down Expand Up @@ -171,7 +171,7 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = {
let SEW_pow_new = get_sew_pow();
if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
vl = EXTZ(0b0);
vl = zeros();
print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
print_reg("CSR vl <- " ^ BitStr(vl));
return RETIRE_SUCCESS
Expand Down
16 changes: 8 additions & 8 deletions model/riscv_insts_zicsr.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,10 +136,10 @@ function readCSR csr : csreg -> xlenbits = {
(0xB82, 32) => minstret[63 .. 32],

/* vector */
(0x008, _) => EXTZ(vstart),
(0x009, _) => EXTZ(vxsat),
(0x00A, _) => EXTZ(vxrm),
(0x00F, _) => EXTZ(vcsr.bits()),
(0x008, _) => zero_extend(vstart),
(0x009, _) => zero_extend(vxsat),
(0x00A, _) => zero_extend(vxrm),
(0x00F, _) => zero_extend(vcsr.bits()),
(0xC20, _) => vl,
(0xC21, _) => vtype.bits(),
(0xC22, _) => vlenb,
Expand Down Expand Up @@ -253,10 +253,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x015, _) => write_seed_csr(),

/* vector */
(0x008, _) => { let vstart_length = get_vlen_pow(); vstart = EXTZ(16, value[(vstart_length - 1) .. 0]); Some(EXTZ(vstart)) },
(0x009, _) => { vxsat = value[0 .. 0]; Some(EXTZ(vxsat)) },
(0x00A, _) => { vxrm = value[1 .. 0]; Some(EXTZ(vxrm)) },
(0x00F, _) => { vcsr->bits() = value[2 ..0]; Some(EXTZ(vcsr.bits())) },
(0x008, _) => { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); Some(zero_extend(vstart)) },
(0x009, _) => { vxsat = value[0 .. 0]; Some(zero_extend(vxsat)) },
(0x00A, _) => { vxrm = value[1 .. 0]; Some(zero_extend(vxrm)) },
(0x00F, _) => { vcsr->bits() = value[2 ..0]; Some(zero_extend(vcsr.bits())) },
(0xC20, _) => { vl = value; Some(vl) },
(0xC21, _) => { vtype->bits() = value; Some(vtype.bits()) },
(0xC22, _) => { vlenb = value; Some(vlenb) },
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -600,19 +600,19 @@ function init_sys() -> unit = {
minstret_increment = true;

/* initialize vector csrs */
vstart = EXTZ(0b0);
vstart = zero_extend(0b0);
vxsat = 0b0;
vxrm = 0b00;
vcsr->vxrm() = vxrm;
vcsr->vxsat() = vxsat;
vl = EXTZ(0b0);
vl = zero_extend(0b0);
vtype->vill() = 0b1;
vtype->reserved() = EXTZ(0b0);
vtype->reserved() = zero_extend(0b0);
vtype->vma() = 0b0;
vtype->vta() = 0b0;
vtype->vsew() = 0b000;
vtype->vlmul() = 0b000;
vlenb = EXTZ(0b0);
vlenb = zero_extend(0b0);

init_pmp();

Expand Down
18 changes: 9 additions & 9 deletions model/riscv_vext_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,14 +45,14 @@ function clause ext_is_CSR_defined (0x009, _) = true
function clause ext_is_CSR_defined (0x00A, _) = true
function clause ext_is_CSR_defined (0x00F, _) = true

function clause ext_read_CSR (0x009) = Some (EXTZ (vcsr.vxsat()))
function clause ext_read_CSR (0x00A) = Some (EXTZ (vcsr.vxrm()))
function clause ext_read_CSR (0x00F) = Some (EXTZ (vcsr.bits()))
function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat()))
function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm()))
function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits()))

function clause ext_read_CSR (0x009) = Some (EXTZ (vcsr.vxsat()))
function clause ext_read_CSR (0x00A) = Some (EXTZ (vcsr.vxrm()))
function clause ext_read_CSR (0x00F) = Some (EXTZ (vcsr.bits()))
function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat()))
function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm()))
function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits()))

function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr.vxrm(), value[0 .. 0]); Some(EXTZ(vcsr.vxsat())) }
function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr.vxsat()); Some(EXTZ(vcsr.vxrm())) }
function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(EXTZ(vcsr.bits())) }
function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr.vxrm(), value[0 .. 0]); Some(zero_extend(vcsr.vxsat())) }
function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr.vxsat()); Some(zero_extend(vcsr.vxrm())) }
function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits())) }
10 changes: 5 additions & 5 deletions model/riscv_vext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ mapping vreg_name = {

val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype effect {rreg, escape}
function rV r = {
let zero_vreg : vregtype = EXTZ(0x0);
let zero_vreg : vregtype = zeros();
let v : vregtype =
match r {
0 => vr0,
Expand Down Expand Up @@ -203,7 +203,7 @@ overload V = {rV_bits, wV_bits, rV, wV}

val init_vregs : unit -> unit effect {wreg}
function init_vregs () = {
let zero_vreg : vregtype = EXTZ(0x0);
let zero_vreg : vregtype = zeros();
vr0 = zero_vreg;
vr1 = zero_vreg;
vr2 = zero_vreg;
Expand Down Expand Up @@ -286,7 +286,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = {
assert(8 <= SEW & SEW <= 64);
foreach (i from (num_elem - 1) downto 0) {
r = r << SEW;
r = r | EXTZ(v[i]);
r = r | zero_extend(v[i]);
};

V(vrid) = r
Expand Down Expand Up @@ -377,9 +377,9 @@ function write_single_element(EEW, index, vrid, value) = {
foreach (i from ('elem_per_reg - 1) downto 0) {
r = r << EEW;
if i == real_index then {
r = r | EXTZ(value);
r = r | zero_extend(value);
} else {
r = r | EXTZ(vrid_val[i]);
r = r | zero_extend(vrid_val[i]);
}
};
V(real_vrid) = r;
Expand Down

0 comments on commit d49437c

Please sign in to comment.