diff options
-rw-r--r-- | model/riscv_insts_vext_mem.sail | 20 | ||||
-rwxr-xr-x | model/riscv_insts_vext_red.sail | 4 | ||||
-rwxr-xr-x | model/riscv_insts_vext_utils.sail | 90 | ||||
-rw-r--r-- | model/riscv_sys_regs.sail | 12 | ||||
-rw-r--r-- | model/riscv_vext_regs.sail | 28 | ||||
-rw-r--r-- | model/riscv_vlen.sail | 4 |
6 files changed, 79 insertions, 79 deletions
diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 292d98f..85adcfd 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -104,7 +104,7 @@ union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if haveVExt() <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() -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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); @@ -170,7 +170,7 @@ union clause ast = VLSEGFFTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if haveVExt() <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() -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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); @@ -275,7 +275,7 @@ union clause ast = VSSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if haveVExt() <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() -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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); @@ -344,7 +344,7 @@ union clause ast = VLSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if haveVExt() <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() -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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); @@ -411,7 +411,7 @@ union clause ast = VSSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if haveVExt() <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() -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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); @@ -481,7 +481,7 @@ union clause ast = VLUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if haveVExt() <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() -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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_data_pow); let width_type : word_width = bytes_wordwidth(EEW_data_bytes); @@ -573,7 +573,7 @@ union clause ast = VSUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if haveVExt() <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() -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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +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 int_power(2, EMUL_data_pow); let width_type : word_width = bytes_wordwidth(EEW_data_bytes); @@ -668,7 +668,7 @@ union clause ast = VLRETYPE : (bits(3), regidx, vlewidth, regidx) mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if haveVExt() <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() -val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); let start_element = get_start_element(); @@ -750,7 +750,7 @@ union clause ast = VSRETYPE : (bits(3), regidx, regidx) mapping clause encdec = VSRETYPE(nf, rs1, vs3) if haveVExt() <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if haveVExt() -val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { let width_type : word_width = BYTE; let start_element = get_start_element(); @@ -855,7 +855,7 @@ mapping encdec_lsop : vmlsop <-> bits(7) = { mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if haveVExt() <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if haveVExt() -val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} +val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { let width_type : word_width = BYTE; let start_element = get_start_element(); diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 6b756f1..be6afc3 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -188,7 +188,7 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = { mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() -val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg} +val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr.FRM(); let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ @@ -227,7 +227,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po RETIRE_SUCCESS } -val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg} +val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr.FRM(); let SEW_widen = SEW * 2; diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index bef5b51..061da54 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -51,7 +51,7 @@ mapping maybe_vmask : string <-> bits(1) = { * 1. vector widening/narrowing instructions * 2. vector load/store instructions */ -val valid_eew_emul : (int, int) -> bool effect {rreg} +val valid_eew_emul : (int, int) -> bool function valid_eew_emul(EEW, EMUL_pow) = { let ELEN = int_power(2, get_elen_pow()); EEW >= 8 & EEW <= ELEN & EMUL_pow >= -3 & EMUL_pow <= 3 @@ -61,13 +61,13 @@ function valid_eew_emul(EEW, EMUL_pow) = { * 1. If the vill bit is set, then any attempt to execute a vector instruction that depends upon vtype will raise an illegal instruction exception. * 2. vset{i}vl{i} and whole-register loads, stores, and moves do not depend upon vtype. */ -val valid_vtype : unit -> bool effect {rreg} +val valid_vtype : unit -> bool function valid_vtype() = { vtype.vill() == 0b0 } /* Check for vstart value */ -val assert_vstart : int -> bool effect {rreg} +val assert_vstart : int -> bool function assert_vstart(i) = { unsigned(vstart) == i } @@ -242,7 +242,7 @@ function illegal_indexed_store(nf, EEW_index, EMUL_pow_index, EMUL_pow_data) = { } /* Scalar register shaping */ -val get_scalar : forall 'm, 'm >= 8. (regidx, int('m)) -> bits('m) effect {escape, rreg} +val get_scalar : forall 'm, 'm >= 8. (regidx, int('m)) -> bits('m) function get_scalar(rs1, SEW) = { if SEW <= sizeof(xlen) then { /* Least significant SEW bits */ @@ -254,7 +254,7 @@ function get_scalar(rs1, SEW) = { } /* Get the starting element index from csr vtype */ -val get_start_element : unit -> nat effect {escape, rreg, wreg} +val get_start_element : unit -> nat function get_start_element() = { let start_element = unsigned(vstart); let VLEN_pow = get_vlen_pow(); @@ -269,7 +269,7 @@ function get_start_element() = { } /* Get the ending element index from csr vl */ -val get_end_element : unit -> int effect {escape, rreg, wreg} +val get_end_element : unit -> int function get_end_element() = unsigned(vl) - 1 /* Mask handling; creates a pre-masked result vector for vstart, vl, vta/vma, and vm */ @@ -280,7 +280,7 @@ function get_end_element() = unsigned(vl) - 1 * vector2 is a "mask" vector that is true for an element if the corresponding element * in the result vector should be updated by the calling instruction */ -val init_masked_result : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) effect {escape, rreg, undef} +val init_masked_result : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); @@ -333,7 +333,7 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { * (vs3 for store and vs2 for reduction). There's no destination register to be masked. * In these cases, this function can be called to simply get the mask vector for vs (without the prepared vd result vector). */ -val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, dec, bool)) -> vector('n, dec, bool) effect {escape, rreg, undef} +val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, dec, bool)) -> vector('n, dec, bool) function init_masked_source(num_elem, LMUL_pow, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); @@ -367,7 +367,7 @@ function init_masked_source(num_elem, LMUL_pow, vm_val) = { /* Mask handling for carry functions that use masks as input/output */ /* Only prestart and tail elements are masked in a mask value */ -val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef} +val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { let start_element = get_start_element(); let end_element = get_end_element(); @@ -403,7 +403,7 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { } /* Mask handling for cmp functions that use masks as output */ -val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef} +val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); @@ -450,7 +450,7 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { * Read multiple register groups and concatenate them in parallel * The whole segments with the same element index are combined together */ -val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, dec, bits('q * 'm)) effect {escape, rreg, undef} +val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, dec, bits('q * 'm)) function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { assert('q * 'm > 0); let LMUL_reg : int = if LMUL_pow <= 0 then 1 else int_power(2, LMUL_pow); @@ -579,7 +579,7 @@ function f_is_NaN(xf) = { } /* Scalar register shaping for floating point operations */ -val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) effect {escape, rreg} +val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) function get_scalar_fp(rs1, SEW) = { assert(sizeof(flen) >= SEW, "invalid vector floating-point type width: FLEN < SEW"); match SEW { @@ -590,7 +590,7 @@ function get_scalar_fp(rs1, SEW) = { } /* Shift amounts */ -val get_shift_amount : forall 'n 'm, 0 <= 'n & 'm in {8, 16, 32, 64}. (bits('n), int('m)) -> nat effect {escape} +val get_shift_amount : forall 'n 'm, 0 <= 'n & 'm in {8, 16, 32, 64}. (bits('n), int('m)) -> nat function get_shift_amount(bit_val, SEW) = { let lowlog2bits = log2(SEW); assert(0 < lowlog2bits & lowlog2bits < 'n); @@ -598,7 +598,7 @@ function get_shift_amount(bit_val, SEW) = { } /* Fixed point rounding increment */ -val get_fixed_rounding_incr : forall ('m 'n : Int), ('m > 0 & 'n >= 0). (bits('m), int('n)) -> bits(1) effect {rreg, undef} +val get_fixed_rounding_incr : forall ('m 'n : Int), ('m > 0 & 'n >= 0). (bits('m), int('n)) -> bits(1) function get_fixed_rounding_incr(vec_elem, shift_amount) = { if shift_amount == 0 then 0b0 else { @@ -615,7 +615,7 @@ function get_fixed_rounding_incr(vec_elem, shift_amount) = { } /* Fixed point unsigned saturation */ -val unsigned_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m) effect {escape, rreg, undef, wreg} +val unsigned_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m) function unsigned_saturation(len, elem) = { if unsigned(elem) > unsigned(ones('m)) then { vxsat = 0b1; @@ -627,7 +627,7 @@ function unsigned_saturation(len, elem) = { } /* Fixed point signed saturation */ -val signed_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m) effect {escape, rreg, undef, wreg} +val signed_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m) function signed_saturation(len, elem) = { if signed(elem) > signed(0b0 @ ones('m - 1)) then { vxsat = 0b1; @@ -642,7 +642,7 @@ function signed_saturation(len, elem) = { } /* Get the floating point rounding mode from csr fcsr */ -val get_fp_rounding_mode : unit -> rounding_mode effect {rreg} +val get_fp_rounding_mode : unit -> rounding_mode function get_fp_rounding_mode() = encdec_rounding_mode(fcsr.FRM()) /* Negate a floating point number */ @@ -656,7 +656,7 @@ function negate_fp(xf) = { } /* Floating point functions using softfloat interface */ -val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) function fp_add(rm_3b, op1, op2) = { let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16Add(rm_3b, op1, op2), @@ -667,7 +667,7 @@ function fp_add(rm_3b, op1, op2) = { result_val } -val fp_sub: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_sub: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) function fp_sub(rm_3b, op1, op2) = { let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16Sub(rm_3b, op1, op2), @@ -678,7 +678,7 @@ function fp_sub(rm_3b, op1, op2) = { result_val } -val fp_min : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_min : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) function fp_min(op1, op2) = { let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Lt_quiet(op1, op2), @@ -697,7 +697,7 @@ function fp_min(op1, op2) = { result_val } -val fp_max : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_max : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) function fp_max(op1, op2) = { let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Lt_quiet(op1, op2), @@ -716,7 +716,7 @@ function fp_max(op1, op2) = { result_val } -val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg} +val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function fp_eq(op1, op2) = { let (fflags, result_val) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Eq(op1, op2), @@ -727,7 +727,7 @@ function fp_eq(op1, op2) = { result_val } -val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg} +val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function fp_gt(op1, op2) = { let (fflags, temp_val) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Le(op1, op2), @@ -739,7 +739,7 @@ function fp_gt(op1, op2) = { result_val } -val fp_ge : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg} +val fp_ge : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function fp_ge(op1, op2) = { let (fflags, temp_val) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Lt(op1, op2), @@ -751,7 +751,7 @@ function fp_ge(op1, op2) = { result_val } -val fp_lt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg} +val fp_lt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function fp_lt(op1, op2) = { let (fflags, result_val) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Lt(op1, op2), @@ -762,7 +762,7 @@ function fp_lt(op1, op2) = { result_val } -val fp_le : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg} +val fp_le : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function fp_le(op1, op2) = { let (fflags, result_val) : (bits_fflags, bool) = match 'm { 16 => riscv_f16Le(op1, op2), @@ -773,7 +773,7 @@ function fp_le(op1, op2) = { result_val } -val fp_mul : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_mul : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) function fp_mul(rm_3b, op1, op2) = { let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16Mul(rm_3b, op1, op2), @@ -784,7 +784,7 @@ function fp_mul(rm_3b, op1, op2) = { result_val } -val fp_div : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_div : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) function fp_div(rm_3b, op1, op2) = { let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16Div(rm_3b, op1, op2), @@ -795,7 +795,7 @@ function fp_div(rm_3b, op1, op2) = { result_val } -val fp_muladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_muladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_muladd(rm_3b, op1, op2, opadd) = { let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16MulAdd(rm_3b, op1, op2, opadd), @@ -806,7 +806,7 @@ function fp_muladd(rm_3b, op1, op2, opadd) = { result_val } -val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_nmuladd(rm_3b, op1, op2, opadd) = { let op1 = negate_fp(op1); let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { @@ -818,7 +818,7 @@ function fp_nmuladd(rm_3b, op1, op2, opadd) = { result_val } -val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_mulsub(rm_3b, op1, op2, opsub) = { let opsub = negate_fp(opsub); let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { @@ -830,7 +830,7 @@ function fp_mulsub(rm_3b, op1, op2, opsub) = { result_val } -val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg} +val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_nmulsub(rm_3b, op1, op2, opsub) = { let opsub = negate_fp(opsub); let op1 = negate_fp(op1); @@ -861,7 +861,7 @@ function fp_class(xf) = { zero_extend(result_val_10b) } -val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) effect {escape, rreg, undef, wreg} +val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) function fp_widen(nval) = { let rm_3b = fcsr.FRM(); let (fflags, wval) : (bits_fflags, bits('m * 2)) = match 'm { @@ -873,7 +873,7 @@ function fp_widen(nval) = { } /* Floating point functions without softfloat support */ -val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) effect {rreg} +val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) function riscv_f16ToI16 (rm, v) = { let (_, sig32) = riscv_f16ToI32(rm, v); if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) @@ -881,7 +881,7 @@ function riscv_f16ToI16 (rm, v) = { else (zeros(5), sig32[15 .. 0]); } -val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) effect {rreg} +val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) function riscv_f16ToI8 (rm, v) = { let (_, sig32) = riscv_f16ToI32(rm, v); if signed(sig32) > signed(0b0 @ ones(7)) then (nvFlag(), 0b0 @ ones(7)) @@ -889,7 +889,7 @@ function riscv_f16ToI8 (rm, v) = { else (zeros(5), sig32[7 .. 0]); } -val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) effect {rreg} +val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) function riscv_f32ToI16 (rm, v) = { let (_, sig32) = riscv_f32ToI32(rm, v); if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) @@ -897,21 +897,21 @@ function riscv_f32ToI16 (rm, v) = { else (zeros(5), sig32[15 .. 0]); } -val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) effect {rreg} +val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) function riscv_f16ToUi16 (rm, v) = { let (_, sig32) = riscv_f16ToUi32(rm, v); if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) else (zeros(5), sig32[15 .. 0]); } -val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) effect {rreg} +val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) function riscv_f16ToUi8 (rm, v) = { let (_, sig32) = riscv_f16ToUi32(rm, v); if unsigned(sig32) > unsigned(ones(8)) then (nvFlag(), ones(8)) else (zeros(5), sig32[7 .. 0]); } -val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) effect {rreg} +val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) function riscv_f32ToUi16 (rm, v) = { let (_, sig32) = riscv_f32ToUi32(rm, v); if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) @@ -974,7 +974,7 @@ function rsqrt7 (v, sub) = { zero_extend(64, sign @ out_exp @ out_sig) } -val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) function riscv_f16Rsqrte7 (rm, v) = { let class = fp_class(v); let (fflags, result) : (bits_fflags, bits_H)= match class { @@ -992,7 +992,7 @@ function riscv_f16Rsqrte7 (rm, v) = { (fflags, result) } -val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) function riscv_f32Rsqrte7 (rm, v) = { let class = fp_class(v); let (fflags, result) : (bits_fflags, bits_S)= match class[15 .. 0] { @@ -1010,7 +1010,7 @@ function riscv_f32Rsqrte7 (rm, v) = { (fflags, result) } -val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) function riscv_f64Rsqrte7 (rm, v) = { let class = fp_class(v); let (fflags, result) : (bits_fflags, bits_D)= match class[15 .. 0] { @@ -1087,7 +1087,7 @@ function recip7 (v, rm_3b, sub) = { } else (false, zero_extend(64, sign @ out_exp @ out_sig)) } -val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) function riscv_f16Recip7 (rm, v) = { let class = fp_class(v); let (round_abnormal_true, res_true) = recip7(v, rm, true); @@ -1106,7 +1106,7 @@ function riscv_f16Recip7 (rm, v) = { (fflags, result) } -val riscv_f32Recip7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Recip7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) function riscv_f32Recip7 (rm, v) = { let class = fp_class(v); let (round_abnormal_true, res_true) = recip7(v, rm, true); @@ -1125,7 +1125,7 @@ function riscv_f32Recip7 (rm, v) = { (fflags, result) } -val riscv_f64Recip7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Recip7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) function riscv_f64Recip7 (rm, v) = { let class = fp_class(v); let (round_abnormal_true, res_true) = recip7(v, rm, true); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index f472ca2..84f708e 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -901,7 +901,7 @@ register vtype : Vtype /* the dynamic selected element width (SEW) */ /* this returns the power of 2 for SEW */ -val get_sew_pow : unit -> {|3, 4, 5, 6|} effect {escape, rreg} +val get_sew_pow : unit -> {|3, 4, 5, 6|} function get_sew_pow() = { let SEW_pow : {|3, 4, 5, 6|} = match vtype.vsew() { 0b000 => 3, @@ -913,7 +913,7 @@ function get_sew_pow() = { SEW_pow } /* this returns the actual value of SEW */ -val get_sew : unit -> {|8, 16, 32, 64|} effect {escape, rreg} +val get_sew : unit -> {|8, 16, 32, 64|} function get_sew() = { match get_sew_pow() { 3 => 8, @@ -923,7 +923,7 @@ function get_sew() = { } } /* this returns the value of SEW in bytes */ -val get_sew_bytes : unit -> {|1, 2, 4, 8|} effect {escape, rreg} +val get_sew_bytes : unit -> {|1, 2, 4, 8|} function get_sew_bytes() = { match get_sew_pow() { 3 => 1, @@ -935,7 +935,7 @@ function get_sew_bytes() = { /* the vector register group multiplier (LMUL) */ /* this returns the power of 2 for LMUL */ -val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|} effect {escape, rreg} +val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|} function get_lmul_pow() = { match vtype.vlmul() { 0b101 => -3, @@ -959,8 +959,8 @@ function decode_agtype(ag) = { } } -val get_vtype_vma : unit -> agtype effect {rreg} +val get_vtype_vma : unit -> agtype function get_vtype_vma() = decode_agtype(vtype.vma()) -val get_vtype_vta : unit -> agtype effect {rreg} +val get_vtype_vta : unit -> agtype function get_vtype_vta() = decode_agtype(vtype.vta()) diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 9b5d6e9..7faa50b 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -116,7 +116,7 @@ function dirty_v_context_if_present() -> unit = { if sys_enable_vext() then dirty_v_context() } -val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype effect {rreg, escape} +val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype function rV r = { let zero_vreg : vregtype = zeros(); let v : vregtype = @@ -158,7 +158,7 @@ function rV r = { v } -val wV : forall 'n, 0 <= 'n < 32. (regno('n), vregtype) -> unit effect {rreg, wreg, escape} +val wV : forall 'n, 0 <= 'n < 32. (regno('n), vregtype) -> unit function wV (r, in_v) = { let v = in_v; match r { @@ -213,7 +213,7 @@ function wV_bits(i: bits(5), data: vregtype) -> unit = { overload V = {rV_bits, wV_bits, rV, wV} -val init_vregs : unit -> unit effect {wreg} +val init_vregs : unit -> unit function init_vregs () = { let zero_vreg : vregtype = zeros(); vr0 = zero_vreg; @@ -257,7 +257,7 @@ bitfield Vcsr : bits(3) = { } register vcsr : Vcsr -val ext_write_vcsr : (bits(2), bits(1)) -> unit effect {rreg, wreg} +val ext_write_vcsr : (bits(2), bits(1)) -> unit function ext_write_vcsr (vxrm_val, vxsat_val) = { vcsr->vxrm() = vxrm_val; /* Note: frm can be an illegal value, 101, 110, 111 */ vcsr->vxsat() = vxsat_val; @@ -265,7 +265,7 @@ 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 effect {escape, rreg} +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; @@ -277,7 +277,7 @@ function get_num_elem(LMUL_pow, SEW) = { } /* Reads a single vreg into multiple elements */ -val read_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef} +val read_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx) -> vector('n, dec, bits('m)) function read_single_vreg(num_elem, SEW, vrid) = { let bv : vregtype = V(vrid); var result : vector('n, dec, bits('m)) = undefined; @@ -292,7 +292,7 @@ function read_single_vreg(num_elem, SEW, vrid) = { } /* Writes multiple elements into a single vreg */ -val write_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx, vector('n, dec, bits('m))) -> unit effect {escape, rreg, wreg} +val write_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx, vector('n, dec, bits('m))) -> unit function write_single_vreg(num_elem, SEW, vrid, v) = { r : vregtype = zeros(); @@ -306,7 +306,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { } /* The general vreg reading operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val read_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef} +val read_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m)) function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { var result : vector('n, dec, bits('m)) = undefined; let VLEN = unsigned(vlenb) * 8; @@ -344,7 +344,7 @@ 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) effect {escape, rreg, undef} +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); @@ -358,7 +358,7 @@ 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. (int('n), int('m), int('p), regidx, vector('n, dec, bits('m))) -> unit effect {escape, rreg, undef, wreg} +val write_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx, vector('n, dec, 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; @@ -381,7 +381,7 @@ 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 effect {escape, rreg, undef, wreg} +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; @@ -403,7 +403,7 @@ function write_single_element(EEW, index, vrid, value) = { } /* Mask register reading operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val read_vmask : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) effect {escape, rreg, undef} +val read_vmask : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) function read_vmask(num_elem, vm, vrid) = { let VLEN = unsigned(vlenb) * 8; assert(num_elem <= sizeof(vlenmax)); @@ -422,7 +422,7 @@ function read_vmask(num_elem, vm, vrid) = { } /* This is a special version of read_vmask for carry/borrow instructions, where vm=1 means no carry */ -val read_vmask_carry : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) effect {escape, rreg, undef} +val read_vmask_carry : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) function read_vmask_carry(num_elem, vm, vrid) = { let VLEN = unsigned(vlenb) * 8; assert(0 < num_elem & num_elem <= sizeof(vlenmax)); @@ -441,7 +441,7 @@ 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, dec, bool)) -> unit effect {escape, rreg, undef, wreg} +val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, dec, bool)) -> unit function write_vmask(num_elem, vrid, v) = { let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); diff --git a/model/riscv_vlen.sail b/model/riscv_vlen.sail index 5e9b375..cd631ba 100644 --- a/model/riscv_vlen.sail +++ b/model/riscv_vlen.sail @@ -38,7 +38,7 @@ register elen : bits(1) -val get_elen_pow : unit -> {|5, 6|} effect {rreg} +val get_elen_pow : unit -> {|5, 6|} function get_elen_pow() = match elen { 0b0 => 5, @@ -51,7 +51,7 @@ function get_elen_pow() = match elen { register vlen : bits(4) -val get_vlen_pow : unit -> {|5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16|} effect {rreg} +val get_vlen_pow : unit -> {|5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16|} function get_vlen_pow() = match vlen { 0b0000 => 5, |