Skip to content

Commit

Permalink
Remove unnecessary brackets
Browse files Browse the repository at this point in the history
  • Loading branch information
@Timmmm
Timmmm committed Dec 6, 2024
1 parent 32b1c56 commit d1edc8e
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 12 deletions.
14 changes: 7 additions & 7 deletions model/riscv_insts_vext_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ex

val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow;
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd);
Expand Down Expand Up @@ -135,7 +135,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(

val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow;
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd);
Expand Down Expand Up @@ -240,7 +240,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E

val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow;
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3);
Expand Down Expand Up @@ -309,7 +309,7 @@ mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnab

val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow;
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd);
Expand Down Expand Up @@ -376,7 +376,7 @@ mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEna

val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow;
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3);
Expand Down Expand Up @@ -446,7 +446,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna

val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow);
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow;
let width_type : word_width = size_bytes(EEW_data_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd);
Expand Down Expand Up @@ -538,7 +538,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn

val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow);
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow;
let width_type : word_width = size_bytes(EEW_data_bytes);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3);
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_vext_utils.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,8 @@ function valid_rd_mask(rd, vm) = {
*/
val valid_reg_overlap : (regidx, regidx, int, int) -> bool
function valid_reg_overlap(rs, rd, EMUL_pow_rs, EMUL_pow_rd) = {
let rs_group = if EMUL_pow_rs > 0 then 2 ^ (EMUL_pow_rs) else 1;
let rd_group = if EMUL_pow_rd > 0 then 2 ^ (EMUL_pow_rd) else 1;
let rs_group = if EMUL_pow_rs > 0 then 2 ^ EMUL_pow_rs else 1;
let rd_group = if EMUL_pow_rd > 0 then 2 ^ EMUL_pow_rd else 1;
let rs_int = unsigned(rs);
let rd_int = unsigned(rd);
if EMUL_pow_rs < EMUL_pow_rd then {
Expand All @@ -79,7 +79,7 @@ function valid_reg_overlap(rs, rd, EMUL_pow_rs, EMUL_pow_rd) = {
val valid_segment : (int, int) -> bool
function valid_segment(nf, EMUL_pow) = {
if EMUL_pow < 0 then nf / (2 ^ (0 - EMUL_pow)) <= 8
else nf * 2 ^ (EMUL_pow) <= 8
else nf * 2 ^ EMUL_pow <= 8
}

/* ******************************************************************************* */
Expand Down Expand Up @@ -371,7 +371,7 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
*/
val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'm >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, bits('q * 'm))
function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = {
let LMUL_reg : int = if LMUL_pow <= 0 then 1 else 2 ^ (LMUL_pow);
let LMUL_reg : int = if LMUL_pow <= 0 then 1 else 2 ^ LMUL_pow;
var vreg_list : vector('q, vector('n, bits('m))) = vector_init(vector_init(zeros()));
var result : vector('n, bits('q * 'm)) = vector_init(zeros());
foreach (j from 0 to (nf - 1)) {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_vext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ function get_num_elem(LMUL_pow, SEW) = {
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 */
let num_elem = 2 ^ (LMUL_pow_reg) * VLEN / SEW;
let num_elem = 2 ^ LMUL_pow_reg * VLEN / SEW;
assert(num_elem > 0);
num_elem
}
Expand Down

0 comments on commit d1edc8e

Please sign in to comment.