diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index e72f91270..0f4da8372 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -44,7 +44,7 @@ function amo_width_valid(size : word_width) -> bool = { union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size) - <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size) + <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) /* We could set load-reservations on physical or virtual addresses. @@ -109,7 +109,7 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx) mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid(size) - <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size) + <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { @@ -207,7 +207,7 @@ mapping encdec_amoop : amoop <-> bits(5) = { } mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(size) - <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size) + <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index caea73a4b..9c4630b33 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -297,8 +297,8 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo /* unsigned loads are only present for widths strictly less than xlen, signed loads also present for widths equal to xlen */ -mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) - <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) +mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes)) + <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes)) val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) function extend_value(is_unsigned, value) = match (value) { @@ -373,8 +373,8 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl) /* ****************************************************************** */ union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool) -mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if word_width_bytes(size) <= sizeof(xlen_bytes) - <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 if word_width_bytes(size) <= sizeof(xlen_bytes) +mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if size_bytes(size) <= sizeof(xlen_bytes) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 942fbaf69..0f1dfeecf 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -61,13 +61,6 @@ mapping vlewidth_pow : vlewidth <-> {|3, 4, 5, 6|} = { VLE64 <-> 6 } -mapping bytes_wordwidth : {|1, 2, 4, 8|} <-> word_width = { - 1 <-> BYTE, - 2 <-> HALF, - 4 <-> WORD, - 8 <-> DOUBLE -} - /* ******************** Vector Load Unit-Stride Normal & Segment (mop=0b00, lumop=0b00000) ********************* */ union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) @@ -77,7 +70,7 @@ mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) 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 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); + let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); @@ -143,7 +136,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) 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 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); + let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let tail_ag : agtype = get_vtype_vta(); @@ -248,7 +241,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) 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 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); + let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); @@ -317,7 +310,7 @@ mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) 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 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); + let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); @@ -384,7 +377,7 @@ mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) 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 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); + let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); @@ -454,7 +447,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) 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 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); + let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); @@ -546,7 +539,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) 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 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); + let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); @@ -640,7 +633,7 @@ mapping clause encdec = VLRETYPE(nf, rs1, width, vd) 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 function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { - let width_type : word_width = bytes_wordwidth(load_width_bytes); + let width_type : word_width = size_bytes(load_width_bytes); let start_element = get_start_element(); if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ let elem_to_align : int = start_element % elem_per_reg; diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 59172cf2e..e9a5a1990 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -367,7 +367,8 @@ mapping bool_not_bits : bool <-> bits(1) = { false <-> 0b1 } -mapping size_bits : word_width <-> bits(2) = { +// Get the bit encoding of word_width. +mapping size_enc : word_width <-> bits(2) = { BYTE <-> 0b00, HALF <-> 0b01, WORD <-> 0b10, @@ -381,12 +382,11 @@ mapping size_mnemonic : word_width <-> string = { DOUBLE <-> "d" } -val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . int('s)} -function word_width_bytes width = match width { - BYTE => 1, - HALF => 2, - WORD => 4, - DOUBLE => 8 +mapping size_bytes : word_width <-> {1, 2, 4, 8} = { + BYTE <-> 1, + HALF <-> 2, + WORD <-> 4, + DOUBLE <-> 8, } /*!