From 520f0194720dda24345b7558c493533dc34e8ceb Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Tue, 8 Oct 2024 19:58:46 +0800 Subject: [PATCH 1/9] Change sign to unsign in v extension --- model/riscv_insts_vext_mem.sail | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 55bcdfd5d..001ad44d4 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -313,7 +313,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e 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); - let rs2_val : int = signed(get_scalar(rs2, xlen)); + let rs2_val : int = unsigned(get_scalar(rs2, xlen)); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); @@ -380,7 +380,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ 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); - let rs2_val : int = signed(get_scalar(rs2, xlen)); + let rs2_val : int = unsigned(get_scalar(rs2, xlen)); let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -459,7 +459,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; + let elem_offset : int = unsigned(vs2_val[i]) + j * EEW_data_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => @@ -550,7 +550,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { - let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; + let elem_offset : int = unsigned(vs2_val[i]) + j * EEW_data_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => From c0319946d67d3c8e7fbcd7f31c023e8823ffd328 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Fri, 25 Oct 2024 12:02:13 +0800 Subject: [PATCH 2/9] remove register vlenb --- model/riscv_insts_vext_mask.sail | 12 ++++++------ model/riscv_insts_vext_mem.sail | 4 ++-- model/riscv_insts_zcmp.sail | 26 ++++++++++++++++++++++++++ model/riscv_sys_control.sail | 5 +---- model/riscv_sys_regs.sail | 5 ++++- model/riscv_vext_control.sail | 3 +-- model/riscv_vext_regs.sail | 14 +++++++------- 7 files changed, 47 insertions(+), 22 deletions(-) create mode 100644 model/riscv_insts_zcmp.sail diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index e4e29a77b..cc35b8df3 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -31,7 +31,7 @@ mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = unsigned(get_vlenb()) * 8; if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; @@ -88,7 +88,7 @@ mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V) function clause execute(VCPOP_M(vm, vs2, rd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = unsigned(get_vlenb()) * 8; if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; @@ -122,7 +122,7 @@ mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V) function clause execute(VFIRST_M(vm, vs2, rd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = unsigned(get_vlenb()) * 8; if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; @@ -158,7 +158,7 @@ mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSBF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = unsigned(get_vlenb()) * 8; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; @@ -198,7 +198,7 @@ mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSIF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = unsigned(get_vlenb()) * 8; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; @@ -238,7 +238,7 @@ mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSOF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(vlenb) * 8; + let num_elem = unsigned(get_vlenb()) * 8; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index cc8161304..1561f530d 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -694,7 +694,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { function clause execute(VLRETYPE(nf, rs1, width, vd)) = { let load_width_bytes = vlewidth_bytesnumber(width); let EEW = load_width_bytes * 8; - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; let elem_per_reg : int = VLEN / EEW; let nf_int = nfields_int(nf); @@ -794,7 +794,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { function clause execute(VSRETYPE(nf, rs1, vs3)) = { let load_width_bytes = 1; let EEW = 8; - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; let elem_per_reg : int = VLEN / EEW; let nf_int = nfields_int(nf); diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail new file mode 100644 index 000000000..d2b67eaac --- /dev/null +++ b/model/riscv_insts_zcmp.sail @@ -0,0 +1,26 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +enum clause extension = Ext_Zcmp +function clause extensionEnabled(Ext_Zcmp) = sys_enable_zcb() + +union clause ast = C_LBU : (bits(2), cregidx, cregidx) + +mapping clause encdec_compressed = + C_LBU(uimm1 @ uimm0, rdc, rs1c) if extensionEnabled(Ext_Zcmp) + <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_Zcmp) + +mapping clause assembly = C_LBU(uimm, rdc, rs1c) <-> + "c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" + +function clause execute C_LBU(uimm, rdc, rs1c) = { + let imm : bits(12) = zero_extend(uimm); + let rd = creg2reg_idx(rdc); + let rs1 = creg2reg_idx(rs1c); + execute(LOAD(imm, rs1, rd, true, BYTE, false, false)) +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 620240cb9..41b51ea57 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -470,10 +470,7 @@ function init_sys() -> unit = { menvcfg.bits = zeros(); senvcfg.bits = zeros(); /* initialize vector csrs */ - vlenb = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */ - /* VLEN value needs to be manually changed currently. - * See riscv_vlen.sail for details. - */ + vstart = zeros(); vl = zeros(); vcsr[vxrm] = 0b00; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 8bbf68e75..e7ca84887 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -799,7 +799,10 @@ function is_fiom_active() -> bool = { /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vl : xlenbits -register vlenb : xlenbits + +function get_vlenb() -> xlenbits = { + to_bits(xlen, (2 ^ (get_vlen_pow()) / 8)) +} bitfield Vtype : xlenbits = { vill : xlen - 1, diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 3dabc1fc0..3795911ab 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -20,7 +20,7 @@ function clause read_CSR(0x00A) = zero_extend(vcsr[vxrm]) function clause read_CSR(0x00F) = zero_extend(vcsr.bits) function clause read_CSR(0xC20) = vl function clause read_CSR(0xC21) = vtype.bits -function clause read_CSR(0xC22) = vlenb +function clause read_CSR(0xC22) = get_vlenb() function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) } function clause write_CSR(0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) } @@ -28,4 +28,3 @@ function clause write_CSR(0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[ function clause write_CSR(0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) } function clause write_CSR(0xC20, value) = { vl = value; vl } function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits } -function clause write_CSR(0xC22, value) = { vlenb = value; vlenb } diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index aadd05bc2..65f288c9d 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -161,7 +161,7 @@ function wV (r : regno, v : vregtype) -> unit = { dirty_v_context(); - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); if get_config_print_reg() then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0])); @@ -229,7 +229,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 function get_num_elem(LMUL_pow, SEW) = { - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; 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 */ @@ -271,7 +271,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, bits('m)) function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { var result : vector('n, bits('m)) = vector_init(zeros()); - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; /* Check for valid vrid */ @@ -308,7 +308,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) function read_single_element(EEW, index, vrid) = { - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; assert(VLEN >= EEW); let 'elem_per_reg : int = VLEN / EEW; assert('elem_per_reg >= 0); @@ -322,7 +322,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 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, bits('m))) -> unit function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; let 'num_elem_single : int = VLEN / SEW; @@ -345,7 +345,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 function write_single_element(EEW, index, vrid, value) = { - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; let 'elem_per_reg : int = VLEN / EEW; assert('elem_per_reg >= 0); let real_vrid : regidx = vrid + to_bits(5, index / 'elem_per_reg); @@ -403,7 +403,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, bool)) -> unit function write_vmask(num_elem, vrid, v) = { - let VLEN = unsigned(vlenb) * 8; + let VLEN = unsigned(get_vlenb()) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); assert(0 < num_elem & num_elem <= VLEN); let vreg_val : vregtype = V(vrid); From 23698cb69f875bc4690291bb961ea5d83d279a32 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Fri, 25 Oct 2024 12:06:58 +0800 Subject: [PATCH 3/9] Revert "remove register vlenb" This reverts commit c0319946d67d3c8e7fbcd7f31c023e8823ffd328. --- model/riscv_insts_vext_mask.sail | 12 ++++++------ model/riscv_insts_vext_mem.sail | 4 ++-- model/riscv_insts_zcmp.sail | 26 -------------------------- model/riscv_sys_control.sail | 5 ++++- model/riscv_sys_regs.sail | 5 +---- model/riscv_vext_control.sail | 3 ++- model/riscv_vext_regs.sail | 14 +++++++------- 7 files changed, 22 insertions(+), 47 deletions(-) delete mode 100644 model/riscv_insts_zcmp.sail diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index cc35b8df3..e4e29a77b 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -31,7 +31,7 @@ mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(get_vlenb()) * 8; + let num_elem = unsigned(vlenb) * 8; if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; @@ -88,7 +88,7 @@ mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V) function clause execute(VCPOP_M(vm, vs2, rd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(get_vlenb()) * 8; + let num_elem = unsigned(vlenb) * 8; if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; @@ -122,7 +122,7 @@ mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V) function clause execute(VFIRST_M(vm, vs2, rd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(get_vlenb()) * 8; + let num_elem = unsigned(vlenb) * 8; if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; @@ -158,7 +158,7 @@ mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSBF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(get_vlenb()) * 8; + let num_elem = unsigned(vlenb) * 8; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; @@ -198,7 +198,7 @@ mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSIF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(get_vlenb()) * 8; + let num_elem = unsigned(vlenb) * 8; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; @@ -238,7 +238,7 @@ mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V) function clause execute(VMSOF_M(vm, vs2, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = unsigned(get_vlenb()) * 8; + let num_elem = unsigned(vlenb) * 8; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 1561f530d..cc8161304 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -694,7 +694,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { function clause execute(VLRETYPE(nf, rs1, width, vd)) = { let load_width_bytes = vlewidth_bytesnumber(width); let EEW = load_width_bytes * 8; - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; let elem_per_reg : int = VLEN / EEW; let nf_int = nfields_int(nf); @@ -794,7 +794,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { function clause execute(VSRETYPE(nf, rs1, vs3)) = { let load_width_bytes = 1; let EEW = 8; - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; let elem_per_reg : int = VLEN / EEW; let nf_int = nfields_int(nf); diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail deleted file mode 100644 index d2b67eaac..000000000 --- a/model/riscv_insts_zcmp.sail +++ /dev/null @@ -1,26 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -enum clause extension = Ext_Zcmp -function clause extensionEnabled(Ext_Zcmp) = sys_enable_zcb() - -union clause ast = C_LBU : (bits(2), cregidx, cregidx) - -mapping clause encdec_compressed = - C_LBU(uimm1 @ uimm0, rdc, rs1c) if extensionEnabled(Ext_Zcmp) - <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_Zcmp) - -mapping clause assembly = C_LBU(uimm, rdc, rs1c) <-> - "c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" - -function clause execute C_LBU(uimm, rdc, rs1c) = { - let imm : bits(12) = zero_extend(uimm); - let rd = creg2reg_idx(rdc); - let rs1 = creg2reg_idx(rs1c); - execute(LOAD(imm, rs1, rd, true, BYTE, false, false)) -} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 41b51ea57..620240cb9 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -470,7 +470,10 @@ function init_sys() -> unit = { menvcfg.bits = zeros(); senvcfg.bits = zeros(); /* initialize vector csrs */ - + vlenb = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */ + /* VLEN value needs to be manually changed currently. + * See riscv_vlen.sail for details. + */ vstart = zeros(); vl = zeros(); vcsr[vxrm] = 0b00; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index e7ca84887..8bbf68e75 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -799,10 +799,7 @@ function is_fiom_active() -> bool = { /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vl : xlenbits - -function get_vlenb() -> xlenbits = { - to_bits(xlen, (2 ^ (get_vlen_pow()) / 8)) -} +register vlenb : xlenbits bitfield Vtype : xlenbits = { vill : xlen - 1, diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 3795911ab..3dabc1fc0 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -20,7 +20,7 @@ function clause read_CSR(0x00A) = zero_extend(vcsr[vxrm]) function clause read_CSR(0x00F) = zero_extend(vcsr.bits) function clause read_CSR(0xC20) = vl function clause read_CSR(0xC21) = vtype.bits -function clause read_CSR(0xC22) = get_vlenb() +function clause read_CSR(0xC22) = vlenb function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) } function clause write_CSR(0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) } @@ -28,3 +28,4 @@ function clause write_CSR(0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[ function clause write_CSR(0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) } function clause write_CSR(0xC20, value) = { vl = value; vl } function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits } +function clause write_CSR(0xC22, value) = { vlenb = value; vlenb } diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 65f288c9d..aadd05bc2 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -161,7 +161,7 @@ function wV (r : regno, v : vregtype) -> unit = { dirty_v_context(); - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); if get_config_print_reg() then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0])); @@ -229,7 +229,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 function get_num_elem(LMUL_pow, SEW) = { - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; 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 */ @@ -271,7 +271,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, bits('m)) function read_vreg(num_elem, SEW, LMUL_pow, vrid) = { var result : vector('n, bits('m)) = vector_init(zeros()); - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; /* Check for valid vrid */ @@ -308,7 +308,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) function read_single_element(EEW, index, vrid) = { - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; assert(VLEN >= EEW); let 'elem_per_reg : int = VLEN / EEW; assert('elem_per_reg >= 0); @@ -322,7 +322,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 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, bits('m))) -> unit function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = { - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; let 'num_elem_single : int = VLEN / SEW; @@ -345,7 +345,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 function write_single_element(EEW, index, vrid, value) = { - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; let 'elem_per_reg : int = VLEN / EEW; assert('elem_per_reg >= 0); let real_vrid : regidx = vrid + to_bits(5, index / 'elem_per_reg); @@ -403,7 +403,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, bool)) -> unit function write_vmask(num_elem, vrid, v) = { - let VLEN = unsigned(get_vlenb()) * 8; + let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); assert(0 < num_elem & num_elem <= VLEN); let vreg_val : vregtype = V(vrid); From 2179dd40b4459b99f2db4255a4f2a41f586dfbc8 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Sun, 3 Nov 2024 10:25:20 +0800 Subject: [PATCH 4/9] Add cm.push --- Makefile | 1 + model/riscv_insts_zcmp.sail | 280 ++++++++++++++++++++++++++++++++++++ 2 files changed, 281 insertions(+) create mode 100644 model/riscv_insts_zcmp.sail diff --git a/Makefile b/Makefile index 119d4e321..2b3057490 100644 --- a/Makefile +++ b/Makefile @@ -24,6 +24,7 @@ SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_mis SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_zifencei.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_hints.sail SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_zcf.sail SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_zcd.sail +SAIL_DEFAULT_INST += riscv_insts_zcmp.sail SAIL_DEFAULT_INST += riscv_insts_svinval.sail diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail new file mode 100644 index 000000000..265755d92 --- /dev/null +++ b/model/riscv_insts_zcmp.sail @@ -0,0 +1,280 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +mapping zcmp_assembly_mapping_32 : (bits(4), bits(2), string) <-> string = { + (0x4, 0b00) <-> "{ra}, -16", + (0x4, 0b01) <-> "{ra}, -32", + (0x4, 0b10) <-> "{ra}, -48", + (0x4, 0b11) <-> "{ra}, -64", + (0x5, 0b00) <-> "{ra, s0}, -16", + (0x5, 0b01) <-> "{ra, s0}, -32", + (0x5, 0b10) <-> "{ra, s0}, -48", + (0x5, 0b11) <-> "{ra, s0}, -64", + (0x6, 0b00) <-> "{ra, s0-s1}, -16", + (0x6, 0b01) <-> "{ra, s0-s1}, -32", + (0x6, 0b10) <-> "{ra, s0-s1}, -48", + (0x6, 0b11) <-> "{ra, s0-s1}, -64", + (0x7, 0b00) <-> "{ra, s0-s2}, -16", + (0x7, 0b01) <-> "{ra, s0-s2}, -32", + (0x7, 0b10) <-> "{ra, s0-s2}, -48", + (0x7, 0b11) <-> "{ra, s0-s2}, -64", + (0x8, 0b00) <-> "{ra, s0-s3}, -32", + (0x8, 0b01) <-> "{ra, s0-s3}, -48", + (0x8, 0b10) <-> "{ra, s0-s3}, -64", + (0x8, 0b11) <-> "{ra, s0-s3}, -80", + (0x9, 0b00) <-> "{ra, s0-s4}, -32", + (0x9, 0b01) <-> "{ra, s0-s4}, -48", + (0x9, 0b10) <-> "{ra, s0-s4}, -64", + (0x9, 0b11) <-> "{ra, s0-s4}, -80", + (0xa, 0b00) <-> "{ra, s0-s5}, -32", + (0xa, 0b01) <-> "{ra, s0-s5}, -48", + (0xa, 0b10) <-> "{ra, s0-s5}, -64", + (0xa, 0b11) <-> "{ra, s0-s5}, -80", + (0xb, 0b00) <-> "{ra, s0-s6}, -32", + (0xb, 0b01) <-> "{ra, s0-s6}, -48", + (0xb, 0b10) <-> "{ra, s0-s6}, -64", + (0xb, 0b11) <-> "{ra, s0-s6}, -80", + (0xc, 0b00) <-> "{ra, s0-s7}, -48", + (0xc, 0b01) <-> "{ra, s0-s7}, -64", + (0xc, 0b10) <-> "{ra, s0-s7}, -80", + (0xc, 0b11) <-> "{ra, s0-s7}, -96", + (0xd, 0b00) <-> "{ra, s0-s8}, -48", + (0xd, 0b01) <-> "{ra, s0-s8}, -64", + (0xd, 0b10) <-> "{ra, s0-s8}, -80", + (0xd, 0b11) <-> "{ra, s0-s8}, -96", + (0xe, 0b00) <-> "{ra, s0-s9}, -48", + (0xe, 0b01) <-> "{ra, s0-s9}, -64", + (0xe, 0b10) <-> "{ra, s0-s9}, -80", + (0xe, 0b11) <-> "{ra, s0-s9}, -96", + (0xf, 0b00) <-> "{ra, s0-11}, -64", + (0xf, 0b01) <-> "{ra, s0-11}, -80", + (0xf, 0b10) <-> "{ra, s0-11}, -96", + (0xf, 0b11) <-> "{ra, s0-11}, -112", +} + +mapping zcmp_assembly_mapping_64 : (bits(4), bits(2)) <-> string = { + (0x4, 0b00) <-> "{ra}, -16", + (0x4, 0b01) <-> "{ra}, -32", + (0x4, 0b10) <-> "{ra}, -48", + (0x4, 0b11) <-> "{ra}, -64", + (0x5, 0b00) <-> "{ra, s0}, -16", + (0x5, 0b01) <-> "{ra, s0}, -32", + (0x5, 0b10) <-> "{ra, s0}, -48", + (0x5, 0b11) <-> "{ra, s0}, -64", + (0x6, 0b00) <-> "{ra, s0-s1}, -32", + (0x6, 0b01) <-> "{ra, s0-s1}, -48", + (0x6, 0b10) <-> "{ra, s0-s1}, -64", + (0x6, 0b11) <-> "{ra, s0-s1}, -80", + (0x7, 0b00) <-> "{ra, s0-s2}, -32", + (0x7, 0b01) <-> "{ra, s0-s2}, -48", + (0x7, 0b10) <-> "{ra, s0-s2}, -64", + (0x7, 0b11) <-> "{ra, s0-s2}, -80", + (0x8, 0b00) <-> "{ra, s0-s3}, -48", + (0x8, 0b01) <-> "{ra, s0-s3}, -64", + (0x8, 0b10) <-> "{ra, s0-s3}, -80", + (0x8, 0b11) <-> "{ra, s0-s3}, -96", + (0x9, 0b00) <-> "{ra, s0-s4}, -48", + (0x9, 0b01) <-> "{ra, s0-s4}, -64", + (0x9, 0b10) <-> "{ra, s0-s4}, -80", + (0x9, 0b11) <-> "{ra, s0-s4}, -96", + (0xa, 0b00) <-> "{ra, s0-s5}, -64", + (0xa, 0b01) <-> "{ra, s0-s5}, -80", + (0xa, 0b10) <-> "{ra, s0-s5}, -96", + (0xa, 0b11) <-> "{ra, s0-s5}, -112", + (0xb, 0b00) <-> "{ra, s0-s6}, -64", + (0xb, 0b01) <-> "{ra, s0-s6}, -80", + (0xb, 0b10) <-> "{ra, s0-s6}, -96", + (0xb, 0b11) <-> "{ra, s0-s6}, -112", + (0xc, 0b00) <-> "{ra, s0-s7}, -80", + (0xc, 0b01) <-> "{ra, s0-s7}, -96", + (0xc, 0b10) <-> "{ra, s0-s7}, -112", + (0xc, 0b11) <-> "{ra, s0-s7}, -128", + (0xd, 0b00) <-> "{ra, s0-s8}, -80", + (0xd, 0b01) <-> "{ra, s0-s8}, -96", + (0xd, 0b10) <-> "{ra, s0-s8}, -112", + (0xd, 0b11) <-> "{ra, s0-s8}, -120", + (0xe, 0b00) <-> "{ra, s0-s9}, -96", + (0xe, 0b01) <-> "{ra, s0-s9}, -112", + (0xe, 0b10) <-> "{ra, s0-s9}, -128", + (0xe, 0b11) <-> "{ra, s0-s9}, -144", + (0xf, 0b00) <-> "{ra, s0-s11}, -112", + (0xf, 0b01) <-> "{ra, s0-s11}, -128", + (0xf, 0b10) <-> "{ra, s0-s11}, -144", + (0xf, 0b11) <-> "{ra, s0-s11}, -160", +} + +function get_stack_adj_base(rlist : bits(4)) -> int = { + if(xlen == 32) then + match(rlist) { + 0b0100 => 16, + 0b0101 => 16, + 0b0110 => 16, + 0b0111 => 16, + 0b1000 => 32, + 0b1001 => 32, + 0b1010 => 32, + 0b1011 => 32, + 0b1100 => 48, + 0b1101 => 48, + 0b1110 => 48, + 0b1111 => 64, + _ => internal_error(__FILE__, __LINE__, "Unsupported rlist: " ^ bits_str(rlist)) + } + else { + match(rlist) { + 0b0100 => 16, + 0b0101 => 16, + 0b0110 => 32, + 0b0111 => 32, + 0b1000 => 48, + 0b1001 => 48, + 0b1010 => 64, + 0b1011 => 64, + 0b1100 => 80, + 0b1101 => 80, + 0b1110 => 96, + 0b1111 => 112, + _ => internal_error(__FILE__, __LINE__, "Unsupported rlist: " ^ bits_str(rlist)) + } + } +} + +mapping reg_list : bits(4) <-> string = { + 0b0000 <-> "", + 0b0001 <-> "", + 0b0010 <-> "", + 0b0011 <-> "", + 0b0100 <-> "ra", + 0b0101 <-> "ra, s0", + 0b0110 <-> "ra, s0-s1", + 0b0111 <-> "ra, s0-s2", + 0b1000 <-> "ra, s0-s3", + 0b1001 <-> "ra, s0-s4", + 0b1010 <-> "ra, s0-s5", + 0b1011 <-> "ra, s0-s6", + 0b1100 <-> "ra, s0-s7", + 0b1101 <-> "ra, s0-s8", + 0b1110 <-> "ra, s0-s9", + 0b1111 <-> "ra, s0-s11", +} + +mapping rlist_to_int : bits(4) <-> int = { + 0b0000 <-> 0, + 0b0001 <-> 1, + 0b0010 <-> 2, + 0b0011 <-> 3, + 0b0100 <-> 4, + 0b0101 <-> 5, + 0b0110 <-> 6, + 0b0111 <-> 7, + 0b1000 <-> 8, + 0b1001 <-> 9, + 0b1010 <-> 10, + 0b1011 <-> 11, + 0b1100 <-> 12, + 0b1101 <-> 13, + 0b1110 <-> 14, + 0b1111 <-> 15, +} + +mapping spimm_to_int : bits(2) <-> int = { + 0b00 <-> 0, + 0b01 <-> 1, + 0b10 <-> 2, + 0b11 <-> 3, +} + +function zcmp_regmask(rlist : bits(4)) -> vector(32, bool) = { + var mask : vector(32, bool) = undefined; + + if(unsigned(rlist) >= unsigned(0b100)) then { + mask[1] = true + }; + + let rlist_num = rlist_to_int(rlist); + + foreach (i from 5 to rlist_num) { + assert(i <= 15); + if( (i - 5) < 2 ) then + mask[3 + i] = true + else { + mask[11 + i] = true + }; + }; + + if(rlist == zero_extend(0xf)) then + mask[27] = true; + + mask +} + +enum clause extension = Ext_Zcmp +function clause extensionEnabled(Ext_Zcmp) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_Zcd) == false & (xlen == 32 | xlen == 64) + +union clause ast = CM_PUSH : (bits(4), bits(2)) + +mapping clause encdec_compressed = CM_PUSH(rlist, spimm) if extensionEnabled(Ext_Zcmp) + <-> 0b101 @ 0b11000 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) + +val process_cmpush : (bits(4), bits(2), word_width) -> Retired +function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) = { + let width_bytes = size_bytes(width); + + let addr = X(sp); + let spimm_int = spimm_to_int(spimm); + let stack_adj = negate_int(get_stack_adj_base(rlist) + spimm_int * 16); + let new_sp = addr + to_bits(xlen, stack_adj); + let mask = zcmp_regmask(rlist); + let bytes = if sizeof(xlen) == 32 then 4 else 8; + + var imm : int = width_bytes; + + foreach (i from 31 downto 1) { + if mask[i] then { + match ext_data_get_addr(sp, to_bits(xlen, negate_int(imm)), Write(Data), xlen / 8) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares = mem_write_ea(paddr, width_bytes, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(_) => { + let reg_val = X(to_bits(5, i)); + match mem_write_value(paddr, width_bytes, reg_val[width_bytes * 8 - 1 .. 0], false, false, false) { + MemValue(true) => { imm = imm + width_bytes }, + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + } + } + } + } + } + } + } + }; + X(sp) = new_sp; + RETIRE_SUCCESS +} + +function clause execute (CM_PUSH(rlist, spimm)) = { + if (xlen == 32) then + process_cmpush(rlist, spimm, WORD) + else + process_cmpush(rlist, spimm, DOUBLE) +} + + +mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 32) <-> + "cm.push" ^ spc() ^ zcmp_assembly_mapping_32(rlist, spimm) if (sizeof(xlen) == 32) + +mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 64) <-> + "cm.push" ^ spc() ^ zcmp_assembly_mapping_64(rlist, spimm) if (sizeof(xlen) == 64) From 57921984339ede0bd9b3a8b8edff9884fa690d3d Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Sun, 3 Nov 2024 23:17:38 +0800 Subject: [PATCH 5/9] Add cm.pop --- model/riscv_insts_zcmp.sail | 62 +++++++++++++++++++++++++++++++++++-- 1 file changed, 60 insertions(+), 2 deletions(-) diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail index 265755d92..69719b70f 100644 --- a/model/riscv_insts_zcmp.sail +++ b/model/riscv_insts_zcmp.sail @@ -6,7 +6,7 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -mapping zcmp_assembly_mapping_32 : (bits(4), bits(2), string) <-> string = { +mapping zcmp_assembly_mapping_32 : (bits(4), bits(2)) <-> string = { (0x4, 0b00) <-> "{ra}, -16", (0x4, 0b01) <-> "{ra}, -32", (0x4, 0b10) <-> "{ra}, -48", @@ -272,9 +272,67 @@ function clause execute (CM_PUSH(rlist, spimm)) = { process_cmpush(rlist, spimm, DOUBLE) } - mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 32) <-> "cm.push" ^ spc() ^ zcmp_assembly_mapping_32(rlist, spimm) if (sizeof(xlen) == 32) mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 64) <-> "cm.push" ^ spc() ^ zcmp_assembly_mapping_64(rlist, spimm) if (sizeof(xlen) == 64) + + +union clause ast = CM_POP : (bits(4), bits(2)) + +mapping clause encdec_compressed = CM_POP(rlist, spimm) if extensionEnabled(Ext_Zcmp) + <-> 0b101 @ 0b11010 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) + +val process_cmpop : (bits(4), bits(2), word_width) -> Retired +function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width) = { + let width_bytes = size_bytes(width); + + let addr = X(sp); + let spimm_int = spimm_to_int(spimm); + let stack_adj = get_stack_adj_base(rlist) + spimm_int * 16; + let new_sp = addr + to_bits(xlen, stack_adj); + let mask = zcmp_regmask(rlist); + let bytes = if sizeof(xlen) == 32 then 4 else 8; + + X(sp) = new_sp; + + var imm : int = width_bytes; + + foreach (i from 31 downto 1) { + if mask[i] then { + match ext_data_get_addr(sp, to_bits(xlen, negate_int(imm)), Write(Data), xlen / 8) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, width_bytes, false, false, false) { + MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + MemValue(v) => { + X(to_bits(5, i)) = extend_value(true, v); + imm = imm + width_bytes + } + } + } + } + } + } + }; + RETIRE_SUCCESS +} + +function clause execute (CM_POP(rlist, spimm)) = { + if (xlen == 32) then + process_cmpop(rlist, spimm, WORD) + else + process_cmpop(rlist, spimm, DOUBLE) +} + +mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 32) <-> + "cm.pop" ^ spc() ^ zcmp_assembly_mapping_32(rlist, spimm) if (sizeof(xlen) == 32) + +mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 64) <-> + "cm.pop" ^ spc() ^ zcmp_assembly_mapping_64(rlist, spimm) if (sizeof(xlen) == 64) From cead192caf2982bd48d304d612ec50176b77b695 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 4 Nov 2024 23:46:12 +0800 Subject: [PATCH 6/9] Add cm.popret cm.popretz --- model/riscv_insts_zcmp.sail | 371 +++++++++++++++++++++++++----------- 1 file changed, 259 insertions(+), 112 deletions(-) diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail index 69719b70f..b48847dd6 100644 --- a/model/riscv_insts_zcmp.sail +++ b/model/riscv_insts_zcmp.sail @@ -6,106 +6,212 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -mapping zcmp_assembly_mapping_32 : (bits(4), bits(2)) <-> string = { - (0x4, 0b00) <-> "{ra}, -16", - (0x4, 0b01) <-> "{ra}, -32", - (0x4, 0b10) <-> "{ra}, -48", - (0x4, 0b11) <-> "{ra}, -64", - (0x5, 0b00) <-> "{ra, s0}, -16", - (0x5, 0b01) <-> "{ra, s0}, -32", - (0x5, 0b10) <-> "{ra, s0}, -48", - (0x5, 0b11) <-> "{ra, s0}, -64", - (0x6, 0b00) <-> "{ra, s0-s1}, -16", - (0x6, 0b01) <-> "{ra, s0-s1}, -32", - (0x6, 0b10) <-> "{ra, s0-s1}, -48", - (0x6, 0b11) <-> "{ra, s0-s1}, -64", - (0x7, 0b00) <-> "{ra, s0-s2}, -16", - (0x7, 0b01) <-> "{ra, s0-s2}, -32", - (0x7, 0b10) <-> "{ra, s0-s2}, -48", - (0x7, 0b11) <-> "{ra, s0-s2}, -64", - (0x8, 0b00) <-> "{ra, s0-s3}, -32", - (0x8, 0b01) <-> "{ra, s0-s3}, -48", - (0x8, 0b10) <-> "{ra, s0-s3}, -64", - (0x8, 0b11) <-> "{ra, s0-s3}, -80", - (0x9, 0b00) <-> "{ra, s0-s4}, -32", - (0x9, 0b01) <-> "{ra, s0-s4}, -48", - (0x9, 0b10) <-> "{ra, s0-s4}, -64", - (0x9, 0b11) <-> "{ra, s0-s4}, -80", - (0xa, 0b00) <-> "{ra, s0-s5}, -32", - (0xa, 0b01) <-> "{ra, s0-s5}, -48", - (0xa, 0b10) <-> "{ra, s0-s5}, -64", - (0xa, 0b11) <-> "{ra, s0-s5}, -80", - (0xb, 0b00) <-> "{ra, s0-s6}, -32", - (0xb, 0b01) <-> "{ra, s0-s6}, -48", - (0xb, 0b10) <-> "{ra, s0-s6}, -64", - (0xb, 0b11) <-> "{ra, s0-s6}, -80", - (0xc, 0b00) <-> "{ra, s0-s7}, -48", - (0xc, 0b01) <-> "{ra, s0-s7}, -64", - (0xc, 0b10) <-> "{ra, s0-s7}, -80", - (0xc, 0b11) <-> "{ra, s0-s7}, -96", - (0xd, 0b00) <-> "{ra, s0-s8}, -48", - (0xd, 0b01) <-> "{ra, s0-s8}, -64", - (0xd, 0b10) <-> "{ra, s0-s8}, -80", - (0xd, 0b11) <-> "{ra, s0-s8}, -96", - (0xe, 0b00) <-> "{ra, s0-s9}, -48", - (0xe, 0b01) <-> "{ra, s0-s9}, -64", - (0xe, 0b10) <-> "{ra, s0-s9}, -80", - (0xe, 0b11) <-> "{ra, s0-s9}, -96", - (0xf, 0b00) <-> "{ra, s0-11}, -64", - (0xf, 0b01) <-> "{ra, s0-11}, -80", - (0xf, 0b10) <-> "{ra, s0-11}, -96", - (0xf, 0b11) <-> "{ra, s0-11}, -112", -} - -mapping zcmp_assembly_mapping_64 : (bits(4), bits(2)) <-> string = { - (0x4, 0b00) <-> "{ra}, -16", - (0x4, 0b01) <-> "{ra}, -32", - (0x4, 0b10) <-> "{ra}, -48", - (0x4, 0b11) <-> "{ra}, -64", - (0x5, 0b00) <-> "{ra, s0}, -16", - (0x5, 0b01) <-> "{ra, s0}, -32", - (0x5, 0b10) <-> "{ra, s0}, -48", - (0x5, 0b11) <-> "{ra, s0}, -64", - (0x6, 0b00) <-> "{ra, s0-s1}, -32", - (0x6, 0b01) <-> "{ra, s0-s1}, -48", - (0x6, 0b10) <-> "{ra, s0-s1}, -64", - (0x6, 0b11) <-> "{ra, s0-s1}, -80", - (0x7, 0b00) <-> "{ra, s0-s2}, -32", - (0x7, 0b01) <-> "{ra, s0-s2}, -48", - (0x7, 0b10) <-> "{ra, s0-s2}, -64", - (0x7, 0b11) <-> "{ra, s0-s2}, -80", - (0x8, 0b00) <-> "{ra, s0-s3}, -48", - (0x8, 0b01) <-> "{ra, s0-s3}, -64", - (0x8, 0b10) <-> "{ra, s0-s3}, -80", - (0x8, 0b11) <-> "{ra, s0-s3}, -96", - (0x9, 0b00) <-> "{ra, s0-s4}, -48", - (0x9, 0b01) <-> "{ra, s0-s4}, -64", - (0x9, 0b10) <-> "{ra, s0-s4}, -80", - (0x9, 0b11) <-> "{ra, s0-s4}, -96", - (0xa, 0b00) <-> "{ra, s0-s5}, -64", - (0xa, 0b01) <-> "{ra, s0-s5}, -80", - (0xa, 0b10) <-> "{ra, s0-s5}, -96", - (0xa, 0b11) <-> "{ra, s0-s5}, -112", - (0xb, 0b00) <-> "{ra, s0-s6}, -64", - (0xb, 0b01) <-> "{ra, s0-s6}, -80", - (0xb, 0b10) <-> "{ra, s0-s6}, -96", - (0xb, 0b11) <-> "{ra, s0-s6}, -112", - (0xc, 0b00) <-> "{ra, s0-s7}, -80", - (0xc, 0b01) <-> "{ra, s0-s7}, -96", - (0xc, 0b10) <-> "{ra, s0-s7}, -112", - (0xc, 0b11) <-> "{ra, s0-s7}, -128", - (0xd, 0b00) <-> "{ra, s0-s8}, -80", - (0xd, 0b01) <-> "{ra, s0-s8}, -96", - (0xd, 0b10) <-> "{ra, s0-s8}, -112", - (0xd, 0b11) <-> "{ra, s0-s8}, -120", - (0xe, 0b00) <-> "{ra, s0-s9}, -96", - (0xe, 0b01) <-> "{ra, s0-s9}, -112", - (0xe, 0b10) <-> "{ra, s0-s9}, -128", - (0xe, 0b11) <-> "{ra, s0-s9}, -144", - (0xf, 0b00) <-> "{ra, s0-s11}, -112", - (0xf, 0b01) <-> "{ra, s0-s11}, -128", - (0xf, 0b10) <-> "{ra, s0-s11}, -144", - (0xf, 0b11) <-> "{ra, s0-s11}, -160", +// first bool represent the stack_adi is positive or negative. +// second bool represent xlen is 32 or 64. +mapping zcmp_assembly_mapping : (bits(4), bits(2), bool, bool) <-> string = { + (0x4, 0b00, true, true) <-> "{ra}, 16", + (0x4, 0b00, true, false) <-> "{ra}, 32", + (0x4, 0b00, false,true) <-> "{ra}, -16", + (0x4, 0b00, false,false) <-> "{ra}, -32", + (0x4, 0b01, true, true) <-> "{ra}, 32", + (0x4, 0b01, true, false) <-> "{ra}, 48", + (0x4, 0b01, false,true) <-> "{ra}, -32", + (0x4, 0b01, false,false) <-> "{ra}, -48", + (0x4, 0b10, true, true) <-> "{ra}, 48", + (0x4, 0b10, true, false) <-> "{ra}, 64", + (0x4, 0b10, false,true) <-> "{ra}, -48", + (0x4, 0b10, false,false) <-> "{ra}, -64", + (0x4, 0b11, true, true) <-> "{ra}, 64", + (0x4, 0b11, true, false) <-> "{ra}, 80", + (0x4, 0b11, false,true) <-> "{ra}, -64", + (0x4, 0b11, false,false) <-> "{ra}, -80", + + (0x5, 0b00, true, true) <-> "{ra, s0}, 16", + (0x5, 0b00, true, false) <-> "{ra, s0}, 32", + (0x5, 0b00, false,true) <-> "{ra, s0}, -16", + (0x5, 0b00, false,false) <-> "{ra, s0}, -32", + (0x5, 0b01, true, true) <-> "{ra, s0}, 32", + (0x5, 0b01, true, false) <-> "{ra, s0}, 48", + (0x5, 0b01, false,true) <-> "{ra, s0}, -32", + (0x5, 0b01, false,false) <-> "{ra, s0}, -48", + (0x5, 0b10, true, true) <-> "{ra, s0}, 48", + (0x5, 0b10, true, false) <-> "{ra, s0}, 64", + (0x5, 0b10, false,true) <-> "{ra, s0}, -48", + (0x5, 0b10, false,false) <-> "{ra, s0}, -64", + (0x5, 0b11, true, true) <-> "{ra, s0}, 64", + (0x5, 0b11, true, false) <-> "{ra, s0}, 80", + (0x5, 0b11, false,true) <-> "{ra, s0}, -64", + (0x5, 0b11, false,false) <-> "{ra, s0}, -80", + + (0x6, 0b00, true, true) <-> "{ra, s0-s1}, -16", + (0x6, 0b00, true, false) <-> "{ra, s0-s1}, -32", + (0x6, 0b00, false,true) <-> "{ra, s0-s1}, --16", + (0x6, 0b00, false,false) <-> "{ra, s0-s1}, --32", + (0x6, 0b01, true, true) <-> "{ra, s0-s1}, -32", + (0x6, 0b01, true, false) <-> "{ra, s0-s1}, -48", + (0x6, 0b01, false,true) <-> "{ra, s0-s1}, --32", + (0x6, 0b01, false,false) <-> "{ra, s0-s1}, --48", + (0x6, 0b10, true, true) <-> "{ra, s0-s1}, -48", + (0x6, 0b10, true, false) <-> "{ra, s0-s1}, -64", + (0x6, 0b10, false,true) <-> "{ra, s0-s1}, --48", + (0x6, 0b10, false,false) <-> "{ra, s0-s1}, --64", + (0x6, 0b11, true, true) <-> "{ra, s0-s1}, -64", + (0x6, 0b11, true, false) <-> "{ra, s0-s1}, -80", + (0x6, 0b11, false,true) <-> "{ra, s0-s1}, --64", + (0x6, 0b11, false,false) <-> "{ra, s0-s1}, --80", + + (0x7, 0b00, true, true) <-> "{ra, s0-s2}, 16", + (0x7, 0b00, true, false) <-> "{ra, s0-s2}, 32", + (0x7, 0b00, false,true) <-> "{ra, s0-s2}, -16", + (0x7, 0b00, false,false) <-> "{ra, s0-s2}, -32", + (0x7, 0b01, true, true) <-> "{ra, s0-s2}, 32", + (0x7, 0b01, true, false) <-> "{ra, s0-s2}, 48", + (0x7, 0b01, false,true) <-> "{ra, s0-s2}, -32", + (0x7, 0b01, false,false) <-> "{ra, s0-s2}, -48", + (0x7, 0b10, true, true) <-> "{ra, s0-s2}, 48", + (0x7, 0b10, true, false) <-> "{ra, s0-s2}, 64", + (0x7, 0b10, false,true) <-> "{ra, s0-s2}, -48", + (0x7, 0b10, false,false) <-> "{ra, s0-s2}, -64", + (0x7, 0b11, true, true) <-> "{ra, s0-s2}, 64", + (0x7, 0b11, true, false) <-> "{ra, s0-s2}, 80", + (0x7, 0b11, false,true) <-> "{ra, s0-s2}, -64", + (0x7, 0b11, false,false) <-> "{ra, s0-s2}, -80", + + (0x8, 0b00, true, true) <-> "{ra, s0-s3}, 32", + (0x8, 0b00, true, false) <-> "{ra, s0-s3}, 48", + (0x8, 0b00, false,true) <-> "{ra, s0-s3}, -32", + (0x8, 0b00, false,false) <-> "{ra, s0-s3}, -48", + (0x8, 0b01, true, true) <-> "{ra, s0-s3}, 48", + (0x8, 0b01, true, false) <-> "{ra, s0-s3}, 64", + (0x8, 0b01, false,true) <-> "{ra, s0-s3}, -48", + (0x8, 0b01, false,false) <-> "{ra, s0-s3}, -64", + (0x8, 0b10, true, true) <-> "{ra, s0-s3}, 64", + (0x8, 0b10, true, false) <-> "{ra, s0-s3}, 80", + (0x8, 0b10, false,true) <-> "{ra, s0-s3}, -64", + (0x8, 0b10, false,false) <-> "{ra, s0-s3}, -80", + (0x8, 0b11, true, true) <-> "{ra, s0-s3}, 80", + (0x8, 0b11, true, false) <-> "{ra, s0-s3}, 96", + (0x8, 0b11, false,true) <-> "{ra, s0-s3}, -80", + (0x8, 0b11, false,false) <-> "{ra, s0-s3}, -96", + + (0x9, 0b00, true, true) <-> "{ra, s0-s4}, 32", + (0x9, 0b00, true, false) <-> "{ra, s0-s4}, 48", + (0x9, 0b00, false,true) <-> "{ra, s0-s4}, -32", + (0x9, 0b00, false,false) <-> "{ra, s0-s4}, -48", + (0x9, 0b01, true, true) <-> "{ra, s0-s4}, 48", + (0x9, 0b01, true, false) <-> "{ra, s0-s4}, 64", + (0x9, 0b01, false,true) <-> "{ra, s0-s4}, -48", + (0x9, 0b01, false,false) <-> "{ra, s0-s4}, -64", + (0x9, 0b10, true, true) <-> "{ra, s0-s4}, 64", + (0x9, 0b10, true, false) <-> "{ra, s0-s4}, 80", + (0x9, 0b10, false,true) <-> "{ra, s0-s4}, -64", + (0x9, 0b10, false,false) <-> "{ra, s0-s4}, -80", + (0x9, 0b11, true, true) <-> "{ra, s0-s4}, 80", + (0x9, 0b11, true, false) <-> "{ra, s0-s4}, 96", + (0x9, 0b11, false,true) <-> "{ra, s0-s4}, -80", + (0x9, 0b11, false,false) <-> "{ra, s0-s4}, -96", + + (0xa, 0b00, true, true) <-> "{ra, s0-s5}, 32", + (0xa, 0b00, true, false) <-> "{ra, s0-s5}, 48", + (0xa, 0b00, false,true) <-> "{ra, s0-s5}, -32", + (0xa, 0b00, false,false) <-> "{ra, s0-s5}, -48", + (0xa, 0b01, true, true) <-> "{ra, s0-s5}, 48", + (0xa, 0b01, true, false) <-> "{ra, s0-s5}, 64", + (0xa, 0b01, false,true) <-> "{ra, s0-s5}, -48", + (0xa, 0b01, false,false) <-> "{ra, s0-s5}, -64", + (0xa, 0b10, true, true) <-> "{ra, s0-s5}, 64", + (0xa, 0b10, true, false) <-> "{ra, s0-s5}, 80", + (0xa, 0b10, false,true) <-> "{ra, s0-s5}, -64", + (0xa, 0b10, false,false) <-> "{ra, s0-s5}, -80", + (0xa, 0b11, true, true) <-> "{ra, s0-s5}, 80", + (0xa, 0b11, true, false) <-> "{ra, s0-s5}, 96", + (0xa, 0b11, false,true) <-> "{ra, s0-s5}, -80", + (0xa, 0b11, false,false) <-> "{ra, s0-s5}, -96", + + (0xb, 0b00, true, true) <-> "{ra, s0-s6}, 32", + (0xb, 0b00, true, false) <-> "{ra, s0-s6}, 48", + (0xb, 0b00, false,true) <-> "{ra, s0-s6}, -32", + (0xb, 0b00, false,false) <-> "{ra, s0-s6}, -48", + (0xb, 0b01, true, true) <-> "{ra, s0-s6}, 48", + (0xb, 0b01, true, false) <-> "{ra, s0-s6}, 64", + (0xb, 0b01, false,true) <-> "{ra, s0-s6}, -48", + (0xb, 0b01, false,false) <-> "{ra, s0-s6}, -64", + (0xb, 0b10, true, true) <-> "{ra, s0-s6}, 64", + (0xb, 0b10, true, false) <-> "{ra, s0-s6}, 80", + (0xb, 0b10, false,true) <-> "{ra, s0-s6}, -64", + (0xb, 0b10, false,false) <-> "{ra, s0-s6}, -80", + (0xb, 0b11, true, true) <-> "{ra, s0-s6}, 80", + (0xb, 0b11, true, false) <-> "{ra, s0-s6}, 96", + (0xb, 0b11, false,true) <-> "{ra, s0-s6}, -80", + (0xb, 0b11, false,false) <-> "{ra, s0-s6}, -96", + + (0xc, 0b00, true, true) <-> "{ra, s0-s7}, 48", + (0xc, 0b00, true, false) <-> "{ra, s0-s7}, 64", + (0xc, 0b00, false,true) <-> "{ra, s0-s7}, -48", + (0xc, 0b00, false,false) <-> "{ra, s0-s7}, -64", + (0xc, 0b01, true, true) <-> "{ra, s0-s7}, 64", + (0xc, 0b01, true, false) <-> "{ra, s0-s7}, 80", + (0xc, 0b01, false,true) <-> "{ra, s0-s7}, -64", + (0xc, 0b01, false,false) <-> "{ra, s0-s7}, -80", + (0xc, 0b10, true, true) <-> "{ra, s0-s7}, 80", + (0xc, 0b10, true, false) <-> "{ra, s0-s7}, 96", + (0xc, 0b10, false,true) <-> "{ra, s0-s7}, -80", + (0xc, 0b10, false,false) <-> "{ra, s0-s7}, -96", + (0xc, 0b11, true, true) <-> "{ra, s0-s7}, 96", + (0xc, 0b11, true, false) <-> "{ra, s0-s7}, 112", + (0xc, 0b11, false,true) <-> "{ra, s0-s7}, -96", + (0xc, 0b11, false,false )<-> "{ra, s0-s7}, -112", + + (0xd, 0b00, true, true) <-> "{ra, s0-s8}, 48", + (0xd, 0b00, true, false) <-> "{ra, s0-s8}, 64", + (0xd, 0b00, false,true) <-> "{ra, s0-s8}, -48", + (0xd, 0b00, false,false) <-> "{ra, s0-s8}, -64", + (0xd, 0b01, true, true) <-> "{ra, s0-s8}, 64", + (0xd, 0b01, true, false) <-> "{ra, s0-s8}, 80", + (0xd, 0b01, false,true) <-> "{ra, s0-s8}, -64", + (0xd, 0b01, false,false) <-> "{ra, s0-s8}, -80", + (0xd, 0b10, true, true) <-> "{ra, s0-s8}, 80", + (0xd, 0b10, true, false) <-> "{ra, s0-s8}, 96", + (0xd, 0b10, false,true) <-> "{ra, s0-s8}, -80", + (0xd, 0b10, false,false) <-> "{ra, s0-s8}, -96", + (0xd, 0b11, true, true) <-> "{ra, s0-s8}, 96", + (0xd, 0b11, true, false) <-> "{ra, s0-s8}, 112", + (0xd, 0b11, false,true) <-> "{ra, s0-s8}, -96", + (0xd, 0b11, false,false) <-> "{ra, s0-s8}, -112", + + (0xe, 0b00, true, true) <-> "{ra, s0-s9}, 48", + (0xe, 0b00, true, false) <-> "{ra, s0-s9}, 64", + (0xe, 0b00, false,true) <-> "{ra, s0-s9}, -48", + (0xe, 0b00, false,false) <-> "{ra, s0-s9}, -64", + (0xe, 0b01, true, true) <-> "{ra, s0-s9}, 64", + (0xe, 0b01, true, false) <-> "{ra, s0-s9}, 80", + (0xe, 0b01, false,true) <-> "{ra, s0-s9}, -64", + (0xe, 0b01, false,false) <-> "{ra, s0-s9}, -80", + (0xe, 0b10, true, true) <-> "{ra, s0-s9}, 80", + (0xe, 0b10, true, false) <-> "{ra, s0-s9}, 96", + (0xe, 0b10, false,true) <-> "{ra, s0-s9}, -80", + (0xe, 0b10, false,false) <-> "{ra, s0-s9}, -96", + (0xe, 0b11, true, true) <-> "{ra, s0-s9}, 96", + (0xe, 0b11, true, false) <-> "{ra, s0-s9}, 112", + (0xe, 0b11, false,true) <-> "{ra, s0-s9}, -96", + (0xe, 0b11, false,false) <-> "{ra, s0-s9}, -112", + + (0xf, 0b00, true, true) <-> "{ra, s0-11}, 64", + (0xf, 0b00, true, false) <-> "{ra, s0-11}, 80", + (0xf, 0b00, false,true) <-> "{ra, s0-11}, -64", + (0xf, 0b00, false,false) <-> "{ra, s0-11}, -80", + (0xf, 0b01, true, true) <-> "{ra, s0-11}, 80", + (0xf, 0b01, true, false) <-> "{ra, s0-11}, 96", + (0xf, 0b01, false,true) <-> "{ra, s0-11}, -80", + (0xf, 0b01, false,false) <-> "{ra, s0-11}, -96", + (0xf, 0b10, true, true) <-> "{ra, s0-11}, 96", + (0xf, 0b10, true, false) <-> "{ra, s0-11}, 112", + (0xf, 0b10, false,true) <-> "{ra, s0-11}, -96", + (0xf, 0b10, false,false) <-> "{ra, s0-11}, -112", + (0xf, 0b11, true, true) <-> "{ra, s0-11}, 112", + (0xf, 0b11, true, false) <-> "{ra, s0-11}, 128", + (0xf, 0b11, false,true) <-> "{ra, s0-11}, -112", + (0xf, 0b11, false,false) <-> "{ra, s0-11}, -128", } function get_stack_adj_base(rlist : bits(4)) -> int = { @@ -145,10 +251,6 @@ function get_stack_adj_base(rlist : bits(4)) -> int = { } mapping reg_list : bits(4) <-> string = { - 0b0000 <-> "", - 0b0001 <-> "", - 0b0010 <-> "", - 0b0011 <-> "", 0b0100 <-> "ra", 0b0101 <-> "ra, s0", 0b0110 <-> "ra, s0-s1", @@ -273,10 +375,10 @@ function clause execute (CM_PUSH(rlist, spimm)) = { } mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 32) <-> - "cm.push" ^ spc() ^ zcmp_assembly_mapping_32(rlist, spimm) if (sizeof(xlen) == 32) + "cm.push" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, false, true) if (sizeof(xlen) == 32) mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 64) <-> - "cm.push" ^ spc() ^ zcmp_assembly_mapping_64(rlist, spimm) if (sizeof(xlen) == 64) + "cm.push" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, false, false) if (sizeof(xlen) == 64) union clause ast = CM_POP : (bits(4), bits(2)) @@ -284,8 +386,8 @@ union clause ast = CM_POP : (bits(4), bits(2)) mapping clause encdec_compressed = CM_POP(rlist, spimm) if extensionEnabled(Ext_Zcmp) <-> 0b101 @ 0b11010 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) -val process_cmpop : (bits(4), bits(2), word_width) -> Retired -function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width) = { +val process_cmpop : (bits(4), bits(2), word_width, bool, bool) -> Retired +function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, write_pc : bool, write_a0 : bool) = { let width_bytes = size_bytes(width); let addr = X(sp); @@ -321,18 +423,63 @@ function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width) = } } }; + + // cm.popret write pc with ra. + if write_pc then { + let ra_val = X(to_bits(5, 1)); + set_next_pc(ra_val); + }; + + // cm.popretz write a0 with zero. + if write_a0 then { + let a0 : regidx = to_bits(5, 10); + X(a0) = to_bits(xlen, 0); + }; + RETIRE_SUCCESS } function clause execute (CM_POP(rlist, spimm)) = { if (xlen == 32) then - process_cmpop(rlist, spimm, WORD) + process_cmpop(rlist, spimm, WORD, false, false) else - process_cmpop(rlist, spimm, DOUBLE) + process_cmpop(rlist, spimm, DOUBLE, false, false) } mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 32) <-> - "cm.pop" ^ spc() ^ zcmp_assembly_mapping_32(rlist, spimm) if (sizeof(xlen) == 32) + "cm.pop" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, true) if (sizeof(xlen) == 32) mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 64) <-> - "cm.pop" ^ spc() ^ zcmp_assembly_mapping_64(rlist, spimm) if (sizeof(xlen) == 64) + "cm.pop" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, false) if (sizeof(xlen) == 64) + + +union clause ast = CM_POPRET : (bits(4), bits(2)) + +mapping clause encdec_compressed = CM_POPRET(rlist, spimm) if extensionEnabled(Ext_Zcmp) + <-> 0b101 @ 0b11110 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) + +function clause execute (CM_POPRET(rlist, spimm)) = { + if (xlen == 32) then + process_cmpop(rlist, spimm, WORD, true, false) + else + process_cmpop(rlist, spimm, DOUBLE, true, false) +} + +mapping clause assembly = CM_POPRET(rlist, spimm) if (sizeof(xlen) == 32) <-> + "cm.popret" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, true) if (sizeof(xlen) == 32) + +mapping clause assembly = CM_POPRET(rlist, spimm) if (sizeof(xlen) == 64) <-> + "cm.popret" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, false) if (sizeof(xlen) == 64) + + +union clause ast = CM_POPRETZ : (bits(4), bits(2)) + +mapping clause encdec_compressed = CM_POPRETZ(rlist, spimm) if extensionEnabled(Ext_Zcmp) + <-> 0b101 @ 0b11100 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) + +function clause execute (CM_POPRETZ(rlist, spimm)) = { + if (xlen == 32) then + process_cmpop(rlist, spimm, WORD, false, true) + else + process_cmpop(rlist, spimm, DOUBLE, false, true) +} From 499b93b596c4361fae21d11990f1e18c2c7ae002 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Tue, 5 Nov 2024 00:37:33 +0800 Subject: [PATCH 7/9] Add cm.popret cm.popretz --- model/riscv_insts_zcmp.sail | 2 ++ 1 file changed, 2 insertions(+) diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail index b48847dd6..68819d63e 100644 --- a/model/riscv_insts_zcmp.sail +++ b/model/riscv_insts_zcmp.sail @@ -326,6 +326,7 @@ mapping clause encdec_compressed = CM_PUSH(rlist, spimm) if extensionEnabled(E val process_cmpush : (bits(4), bits(2), word_width) -> Retired function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) = { let width_bytes = size_bytes(width); + assert(width_bytes <= xlen_bytes); let addr = X(sp); let spimm_int = spimm_to_int(spimm); @@ -389,6 +390,7 @@ mapping clause encdec_compressed = CM_POP(rlist, spimm) if extensionEnabled(Ex val process_cmpop : (bits(4), bits(2), word_width, bool, bool) -> Retired function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, write_pc : bool, write_a0 : bool) = { let width_bytes = size_bytes(width); + assert(width_bytes <= xlen_bytes); let addr = X(sp); let spimm_int = spimm_to_int(spimm); From b2e8ddb3c3dd44278f79cfff176b79c6432152b5 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Thu, 7 Nov 2024 01:59:40 +0800 Subject: [PATCH 8/9] Add cm.mvsa01 cm.mva01s and some changes --- model/riscv_insts_zcmp.sail | 549 +++++++++++++++++++----------------- 1 file changed, 294 insertions(+), 255 deletions(-) diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail index 68819d63e..4609ebff0 100644 --- a/model/riscv_insts_zcmp.sail +++ b/model/riscv_insts_zcmp.sail @@ -8,244 +8,229 @@ // first bool represent the stack_adi is positive or negative. // second bool represent xlen is 32 or 64. -mapping zcmp_assembly_mapping : (bits(4), bits(2), bool, bool) <-> string = { - (0x4, 0b00, true, true) <-> "{ra}, 16", - (0x4, 0b00, true, false) <-> "{ra}, 32", - (0x4, 0b00, false,true) <-> "{ra}, -16", - (0x4, 0b00, false,false) <-> "{ra}, -32", - (0x4, 0b01, true, true) <-> "{ra}, 32", - (0x4, 0b01, true, false) <-> "{ra}, 48", - (0x4, 0b01, false,true) <-> "{ra}, -32", - (0x4, 0b01, false,false) <-> "{ra}, -48", - (0x4, 0b10, true, true) <-> "{ra}, 48", - (0x4, 0b10, true, false) <-> "{ra}, 64", - (0x4, 0b10, false,true) <-> "{ra}, -48", - (0x4, 0b10, false,false) <-> "{ra}, -64", - (0x4, 0b11, true, true) <-> "{ra}, 64", - (0x4, 0b11, true, false) <-> "{ra}, 80", - (0x4, 0b11, false,true) <-> "{ra}, -64", - (0x4, 0b11, false,false) <-> "{ra}, -80", - - (0x5, 0b00, true, true) <-> "{ra, s0}, 16", - (0x5, 0b00, true, false) <-> "{ra, s0}, 32", - (0x5, 0b00, false,true) <-> "{ra, s0}, -16", - (0x5, 0b00, false,false) <-> "{ra, s0}, -32", - (0x5, 0b01, true, true) <-> "{ra, s0}, 32", - (0x5, 0b01, true, false) <-> "{ra, s0}, 48", - (0x5, 0b01, false,true) <-> "{ra, s0}, -32", - (0x5, 0b01, false,false) <-> "{ra, s0}, -48", - (0x5, 0b10, true, true) <-> "{ra, s0}, 48", - (0x5, 0b10, true, false) <-> "{ra, s0}, 64", - (0x5, 0b10, false,true) <-> "{ra, s0}, -48", - (0x5, 0b10, false,false) <-> "{ra, s0}, -64", - (0x5, 0b11, true, true) <-> "{ra, s0}, 64", - (0x5, 0b11, true, false) <-> "{ra, s0}, 80", - (0x5, 0b11, false,true) <-> "{ra, s0}, -64", - (0x5, 0b11, false,false) <-> "{ra, s0}, -80", - - (0x6, 0b00, true, true) <-> "{ra, s0-s1}, -16", - (0x6, 0b00, true, false) <-> "{ra, s0-s1}, -32", - (0x6, 0b00, false,true) <-> "{ra, s0-s1}, --16", - (0x6, 0b00, false,false) <-> "{ra, s0-s1}, --32", - (0x6, 0b01, true, true) <-> "{ra, s0-s1}, -32", - (0x6, 0b01, true, false) <-> "{ra, s0-s1}, -48", - (0x6, 0b01, false,true) <-> "{ra, s0-s1}, --32", - (0x6, 0b01, false,false) <-> "{ra, s0-s1}, --48", - (0x6, 0b10, true, true) <-> "{ra, s0-s1}, -48", - (0x6, 0b10, true, false) <-> "{ra, s0-s1}, -64", - (0x6, 0b10, false,true) <-> "{ra, s0-s1}, --48", - (0x6, 0b10, false,false) <-> "{ra, s0-s1}, --64", - (0x6, 0b11, true, true) <-> "{ra, s0-s1}, -64", - (0x6, 0b11, true, false) <-> "{ra, s0-s1}, -80", - (0x6, 0b11, false,true) <-> "{ra, s0-s1}, --64", - (0x6, 0b11, false,false) <-> "{ra, s0-s1}, --80", - - (0x7, 0b00, true, true) <-> "{ra, s0-s2}, 16", - (0x7, 0b00, true, false) <-> "{ra, s0-s2}, 32", - (0x7, 0b00, false,true) <-> "{ra, s0-s2}, -16", - (0x7, 0b00, false,false) <-> "{ra, s0-s2}, -32", - (0x7, 0b01, true, true) <-> "{ra, s0-s2}, 32", - (0x7, 0b01, true, false) <-> "{ra, s0-s2}, 48", - (0x7, 0b01, false,true) <-> "{ra, s0-s2}, -32", - (0x7, 0b01, false,false) <-> "{ra, s0-s2}, -48", - (0x7, 0b10, true, true) <-> "{ra, s0-s2}, 48", - (0x7, 0b10, true, false) <-> "{ra, s0-s2}, 64", - (0x7, 0b10, false,true) <-> "{ra, s0-s2}, -48", - (0x7, 0b10, false,false) <-> "{ra, s0-s2}, -64", - (0x7, 0b11, true, true) <-> "{ra, s0-s2}, 64", - (0x7, 0b11, true, false) <-> "{ra, s0-s2}, 80", - (0x7, 0b11, false,true) <-> "{ra, s0-s2}, -64", - (0x7, 0b11, false,false) <-> "{ra, s0-s2}, -80", - - (0x8, 0b00, true, true) <-> "{ra, s0-s3}, 32", - (0x8, 0b00, true, false) <-> "{ra, s0-s3}, 48", - (0x8, 0b00, false,true) <-> "{ra, s0-s3}, -32", - (0x8, 0b00, false,false) <-> "{ra, s0-s3}, -48", - (0x8, 0b01, true, true) <-> "{ra, s0-s3}, 48", - (0x8, 0b01, true, false) <-> "{ra, s0-s3}, 64", - (0x8, 0b01, false,true) <-> "{ra, s0-s3}, -48", - (0x8, 0b01, false,false) <-> "{ra, s0-s3}, -64", - (0x8, 0b10, true, true) <-> "{ra, s0-s3}, 64", - (0x8, 0b10, true, false) <-> "{ra, s0-s3}, 80", - (0x8, 0b10, false,true) <-> "{ra, s0-s3}, -64", - (0x8, 0b10, false,false) <-> "{ra, s0-s3}, -80", - (0x8, 0b11, true, true) <-> "{ra, s0-s3}, 80", - (0x8, 0b11, true, false) <-> "{ra, s0-s3}, 96", - (0x8, 0b11, false,true) <-> "{ra, s0-s3}, -80", - (0x8, 0b11, false,false) <-> "{ra, s0-s3}, -96", - - (0x9, 0b00, true, true) <-> "{ra, s0-s4}, 32", - (0x9, 0b00, true, false) <-> "{ra, s0-s4}, 48", - (0x9, 0b00, false,true) <-> "{ra, s0-s4}, -32", - (0x9, 0b00, false,false) <-> "{ra, s0-s4}, -48", - (0x9, 0b01, true, true) <-> "{ra, s0-s4}, 48", - (0x9, 0b01, true, false) <-> "{ra, s0-s4}, 64", - (0x9, 0b01, false,true) <-> "{ra, s0-s4}, -48", - (0x9, 0b01, false,false) <-> "{ra, s0-s4}, -64", - (0x9, 0b10, true, true) <-> "{ra, s0-s4}, 64", - (0x9, 0b10, true, false) <-> "{ra, s0-s4}, 80", - (0x9, 0b10, false,true) <-> "{ra, s0-s4}, -64", - (0x9, 0b10, false,false) <-> "{ra, s0-s4}, -80", - (0x9, 0b11, true, true) <-> "{ra, s0-s4}, 80", - (0x9, 0b11, true, false) <-> "{ra, s0-s4}, 96", - (0x9, 0b11, false,true) <-> "{ra, s0-s4}, -80", - (0x9, 0b11, false,false) <-> "{ra, s0-s4}, -96", - - (0xa, 0b00, true, true) <-> "{ra, s0-s5}, 32", - (0xa, 0b00, true, false) <-> "{ra, s0-s5}, 48", - (0xa, 0b00, false,true) <-> "{ra, s0-s5}, -32", - (0xa, 0b00, false,false) <-> "{ra, s0-s5}, -48", - (0xa, 0b01, true, true) <-> "{ra, s0-s5}, 48", - (0xa, 0b01, true, false) <-> "{ra, s0-s5}, 64", - (0xa, 0b01, false,true) <-> "{ra, s0-s5}, -48", - (0xa, 0b01, false,false) <-> "{ra, s0-s5}, -64", - (0xa, 0b10, true, true) <-> "{ra, s0-s5}, 64", - (0xa, 0b10, true, false) <-> "{ra, s0-s5}, 80", - (0xa, 0b10, false,true) <-> "{ra, s0-s5}, -64", - (0xa, 0b10, false,false) <-> "{ra, s0-s5}, -80", - (0xa, 0b11, true, true) <-> "{ra, s0-s5}, 80", - (0xa, 0b11, true, false) <-> "{ra, s0-s5}, 96", - (0xa, 0b11, false,true) <-> "{ra, s0-s5}, -80", - (0xa, 0b11, false,false) <-> "{ra, s0-s5}, -96", - - (0xb, 0b00, true, true) <-> "{ra, s0-s6}, 32", - (0xb, 0b00, true, false) <-> "{ra, s0-s6}, 48", - (0xb, 0b00, false,true) <-> "{ra, s0-s6}, -32", - (0xb, 0b00, false,false) <-> "{ra, s0-s6}, -48", - (0xb, 0b01, true, true) <-> "{ra, s0-s6}, 48", - (0xb, 0b01, true, false) <-> "{ra, s0-s6}, 64", - (0xb, 0b01, false,true) <-> "{ra, s0-s6}, -48", - (0xb, 0b01, false,false) <-> "{ra, s0-s6}, -64", - (0xb, 0b10, true, true) <-> "{ra, s0-s6}, 64", - (0xb, 0b10, true, false) <-> "{ra, s0-s6}, 80", - (0xb, 0b10, false,true) <-> "{ra, s0-s6}, -64", - (0xb, 0b10, false,false) <-> "{ra, s0-s6}, -80", - (0xb, 0b11, true, true) <-> "{ra, s0-s6}, 80", - (0xb, 0b11, true, false) <-> "{ra, s0-s6}, 96", - (0xb, 0b11, false,true) <-> "{ra, s0-s6}, -80", - (0xb, 0b11, false,false) <-> "{ra, s0-s6}, -96", - - (0xc, 0b00, true, true) <-> "{ra, s0-s7}, 48", - (0xc, 0b00, true, false) <-> "{ra, s0-s7}, 64", - (0xc, 0b00, false,true) <-> "{ra, s0-s7}, -48", - (0xc, 0b00, false,false) <-> "{ra, s0-s7}, -64", - (0xc, 0b01, true, true) <-> "{ra, s0-s7}, 64", - (0xc, 0b01, true, false) <-> "{ra, s0-s7}, 80", - (0xc, 0b01, false,true) <-> "{ra, s0-s7}, -64", - (0xc, 0b01, false,false) <-> "{ra, s0-s7}, -80", - (0xc, 0b10, true, true) <-> "{ra, s0-s7}, 80", - (0xc, 0b10, true, false) <-> "{ra, s0-s7}, 96", - (0xc, 0b10, false,true) <-> "{ra, s0-s7}, -80", - (0xc, 0b10, false,false) <-> "{ra, s0-s7}, -96", - (0xc, 0b11, true, true) <-> "{ra, s0-s7}, 96", - (0xc, 0b11, true, false) <-> "{ra, s0-s7}, 112", - (0xc, 0b11, false,true) <-> "{ra, s0-s7}, -96", - (0xc, 0b11, false,false )<-> "{ra, s0-s7}, -112", - - (0xd, 0b00, true, true) <-> "{ra, s0-s8}, 48", - (0xd, 0b00, true, false) <-> "{ra, s0-s8}, 64", - (0xd, 0b00, false,true) <-> "{ra, s0-s8}, -48", - (0xd, 0b00, false,false) <-> "{ra, s0-s8}, -64", - (0xd, 0b01, true, true) <-> "{ra, s0-s8}, 64", - (0xd, 0b01, true, false) <-> "{ra, s0-s8}, 80", - (0xd, 0b01, false,true) <-> "{ra, s0-s8}, -64", - (0xd, 0b01, false,false) <-> "{ra, s0-s8}, -80", - (0xd, 0b10, true, true) <-> "{ra, s0-s8}, 80", - (0xd, 0b10, true, false) <-> "{ra, s0-s8}, 96", - (0xd, 0b10, false,true) <-> "{ra, s0-s8}, -80", - (0xd, 0b10, false,false) <-> "{ra, s0-s8}, -96", - (0xd, 0b11, true, true) <-> "{ra, s0-s8}, 96", - (0xd, 0b11, true, false) <-> "{ra, s0-s8}, 112", - (0xd, 0b11, false,true) <-> "{ra, s0-s8}, -96", - (0xd, 0b11, false,false) <-> "{ra, s0-s8}, -112", - - (0xe, 0b00, true, true) <-> "{ra, s0-s9}, 48", - (0xe, 0b00, true, false) <-> "{ra, s0-s9}, 64", - (0xe, 0b00, false,true) <-> "{ra, s0-s9}, -48", - (0xe, 0b00, false,false) <-> "{ra, s0-s9}, -64", - (0xe, 0b01, true, true) <-> "{ra, s0-s9}, 64", - (0xe, 0b01, true, false) <-> "{ra, s0-s9}, 80", - (0xe, 0b01, false,true) <-> "{ra, s0-s9}, -64", - (0xe, 0b01, false,false) <-> "{ra, s0-s9}, -80", - (0xe, 0b10, true, true) <-> "{ra, s0-s9}, 80", - (0xe, 0b10, true, false) <-> "{ra, s0-s9}, 96", - (0xe, 0b10, false,true) <-> "{ra, s0-s9}, -80", - (0xe, 0b10, false,false) <-> "{ra, s0-s9}, -96", - (0xe, 0b11, true, true) <-> "{ra, s0-s9}, 96", - (0xe, 0b11, true, false) <-> "{ra, s0-s9}, 112", - (0xe, 0b11, false,true) <-> "{ra, s0-s9}, -96", - (0xe, 0b11, false,false) <-> "{ra, s0-s9}, -112", - - (0xf, 0b00, true, true) <-> "{ra, s0-11}, 64", - (0xf, 0b00, true, false) <-> "{ra, s0-11}, 80", - (0xf, 0b00, false,true) <-> "{ra, s0-11}, -64", - (0xf, 0b00, false,false) <-> "{ra, s0-11}, -80", - (0xf, 0b01, true, true) <-> "{ra, s0-11}, 80", - (0xf, 0b01, true, false) <-> "{ra, s0-11}, 96", - (0xf, 0b01, false,true) <-> "{ra, s0-11}, -80", - (0xf, 0b01, false,false) <-> "{ra, s0-11}, -96", - (0xf, 0b10, true, true) <-> "{ra, s0-11}, 96", - (0xf, 0b10, true, false) <-> "{ra, s0-11}, 112", - (0xf, 0b10, false,true) <-> "{ra, s0-11}, -96", - (0xf, 0b10, false,false) <-> "{ra, s0-11}, -112", - (0xf, 0b11, true, true) <-> "{ra, s0-11}, 112", - (0xf, 0b11, true, false) <-> "{ra, s0-11}, 128", - (0xf, 0b11, false,true) <-> "{ra, s0-11}, -112", - (0xf, 0b11, false,false) <-> "{ra, s0-11}, -128", +mapping zcmp_assembly_mapping : (bits(4), bits(2), bool, {32, 64}) <-> string = { + (0x4, 0b00, true, 32) <-> "{ra}, 16", + (0x4, 0b00, true, 64) <-> "{ra}, 32", + (0x4, 0b00, false,32) <-> "{ra}, -16", + (0x4, 0b00, false,64) <-> "{ra}, -32", + (0x4, 0b01, true, 32) <-> "{ra}, 32", + (0x4, 0b01, true, 64) <-> "{ra}, 48", + (0x4, 0b01, false,32) <-> "{ra}, -32", + (0x4, 0b01, false,64) <-> "{ra}, -48", + (0x4, 0b10, true, 32) <-> "{ra}, 48", + (0x4, 0b10, true, 64) <-> "{ra}, 64", + (0x4, 0b10, false,32) <-> "{ra}, -48", + (0x4, 0b10, false,64) <-> "{ra}, -64", + (0x4, 0b11, true, 32) <-> "{ra}, 64", + (0x4, 0b11, true, 64) <-> "{ra}, 80", + (0x4, 0b11, false,32) <-> "{ra}, -64", + (0x4, 0b11, false,64) <-> "{ra}, -80", + + (0x5, 0b00, true, 32) <-> "{ra, s0}, 16", + (0x5, 0b00, true, 64) <-> "{ra, s0}, 32", + (0x5, 0b00, false,32) <-> "{ra, s0}, -16", + (0x5, 0b00, false,64) <-> "{ra, s0}, -32", + (0x5, 0b01, true, 32) <-> "{ra, s0}, 32", + (0x5, 0b01, true, 64) <-> "{ra, s0}, 48", + (0x5, 0b01, false,32) <-> "{ra, s0}, -32", + (0x5, 0b01, false,64) <-> "{ra, s0}, -48", + (0x5, 0b10, true, 32) <-> "{ra, s0}, 48", + (0x5, 0b10, true, 64) <-> "{ra, s0}, 64", + (0x5, 0b10, false,32) <-> "{ra, s0}, -48", + (0x5, 0b10, false,64) <-> "{ra, s0}, -64", + (0x5, 0b11, true, 32) <-> "{ra, s0}, 64", + (0x5, 0b11, true, 64) <-> "{ra, s0}, 80", + (0x5, 0b11, false,32) <-> "{ra, s0}, -64", + (0x5, 0b11, false,64) <-> "{ra, s0}, -80", + + (0x6, 0b00, true, 32) <-> "{ra, s0-s1}, -16", + (0x6, 0b00, true, 64) <-> "{ra, s0-s1}, -32", + (0x6, 0b00, false,32) <-> "{ra, s0-s1}, --16", + (0x6, 0b00, false,64) <-> "{ra, s0-s1}, --32", + (0x6, 0b01, true, 32) <-> "{ra, s0-s1}, -32", + (0x6, 0b01, true, 64) <-> "{ra, s0-s1}, -48", + (0x6, 0b01, false,32) <-> "{ra, s0-s1}, --32", + (0x6, 0b01, false,64) <-> "{ra, s0-s1}, --48", + (0x6, 0b10, true, 32) <-> "{ra, s0-s1}, -48", + (0x6, 0b10, true, 64) <-> "{ra, s0-s1}, -64", + (0x6, 0b10, false,32) <-> "{ra, s0-s1}, --48", + (0x6, 0b10, false,64) <-> "{ra, s0-s1}, --64", + (0x6, 0b11, true, 32) <-> "{ra, s0-s1}, -64", + (0x6, 0b11, true, 64) <-> "{ra, s0-s1}, -80", + (0x6, 0b11, false,32) <-> "{ra, s0-s1}, --64", + (0x6, 0b11, false,64) <-> "{ra, s0-s1}, --80", + + (0x7, 0b00, true, 32) <-> "{ra, s0-s2}, 16", + (0x7, 0b00, true, 64) <-> "{ra, s0-s2}, 32", + (0x7, 0b00, false,32) <-> "{ra, s0-s2}, -16", + (0x7, 0b00, false,64) <-> "{ra, s0-s2}, -32", + (0x7, 0b01, true, 32) <-> "{ra, s0-s2}, 32", + (0x7, 0b01, true, 64) <-> "{ra, s0-s2}, 48", + (0x7, 0b01, false,32) <-> "{ra, s0-s2}, -32", + (0x7, 0b01, false,64) <-> "{ra, s0-s2}, -48", + (0x7, 0b10, true, 32) <-> "{ra, s0-s2}, 48", + (0x7, 0b10, true, 64) <-> "{ra, s0-s2}, 64", + (0x7, 0b10, false,32) <-> "{ra, s0-s2}, -48", + (0x7, 0b10, false,64) <-> "{ra, s0-s2}, -64", + (0x7, 0b11, true, 32) <-> "{ra, s0-s2}, 64", + (0x7, 0b11, true, 64) <-> "{ra, s0-s2}, 80", + (0x7, 0b11, false,32) <-> "{ra, s0-s2}, -64", + (0x7, 0b11, false,64) <-> "{ra, s0-s2}, -80", + + (0x8, 0b00, true, 32) <-> "{ra, s0-s3}, 32", + (0x8, 0b00, true, 64) <-> "{ra, s0-s3}, 48", + (0x8, 0b00, false,32) <-> "{ra, s0-s3}, -32", + (0x8, 0b00, false,64) <-> "{ra, s0-s3}, -48", + (0x8, 0b01, true, 32) <-> "{ra, s0-s3}, 48", + (0x8, 0b01, true, 64) <-> "{ra, s0-s3}, 64", + (0x8, 0b01, false,32) <-> "{ra, s0-s3}, -48", + (0x8, 0b01, false,64) <-> "{ra, s0-s3}, -64", + (0x8, 0b10, true, 32) <-> "{ra, s0-s3}, 64", + (0x8, 0b10, true, 64) <-> "{ra, s0-s3}, 80", + (0x8, 0b10, false,32) <-> "{ra, s0-s3}, -64", + (0x8, 0b10, false,64) <-> "{ra, s0-s3}, -80", + (0x8, 0b11, true, 32) <-> "{ra, s0-s3}, 80", + (0x8, 0b11, true, 64) <-> "{ra, s0-s3}, 96", + (0x8, 0b11, false,32) <-> "{ra, s0-s3}, -80", + (0x8, 0b11, false,64) <-> "{ra, s0-s3}, -96", + + (0x9, 0b00, true, 32) <-> "{ra, s0-s4}, 32", + (0x9, 0b00, true, 64) <-> "{ra, s0-s4}, 48", + (0x9, 0b00, false,32) <-> "{ra, s0-s4}, -32", + (0x9, 0b00, false,64) <-> "{ra, s0-s4}, -48", + (0x9, 0b01, true, 32) <-> "{ra, s0-s4}, 48", + (0x9, 0b01, true, 64) <-> "{ra, s0-s4}, 64", + (0x9, 0b01, false,32) <-> "{ra, s0-s4}, -48", + (0x9, 0b01, false,64) <-> "{ra, s0-s4}, -64", + (0x9, 0b10, true, 32) <-> "{ra, s0-s4}, 64", + (0x9, 0b10, true, 64) <-> "{ra, s0-s4}, 80", + (0x9, 0b10, false,32) <-> "{ra, s0-s4}, -64", + (0x9, 0b10, false,64) <-> "{ra, s0-s4}, -80", + (0x9, 0b11, true, 32) <-> "{ra, s0-s4}, 80", + (0x9, 0b11, true, 64) <-> "{ra, s0-s4}, 96", + (0x9, 0b11, false,32) <-> "{ra, s0-s4}, -80", + (0x9, 0b11, false,64) <-> "{ra, s0-s4}, -96", + + (0xa, 0b00, true, 32) <-> "{ra, s0-s5}, 32", + (0xa, 0b00, true, 64) <-> "{ra, s0-s5}, 48", + (0xa, 0b00, false,32) <-> "{ra, s0-s5}, -32", + (0xa, 0b00, false,64) <-> "{ra, s0-s5}, -48", + (0xa, 0b01, true, 32) <-> "{ra, s0-s5}, 48", + (0xa, 0b01, true, 64) <-> "{ra, s0-s5}, 64", + (0xa, 0b01, false,32) <-> "{ra, s0-s5}, -48", + (0xa, 0b01, false,64) <-> "{ra, s0-s5}, -64", + (0xa, 0b10, true, 32) <-> "{ra, s0-s5}, 64", + (0xa, 0b10, true, 64) <-> "{ra, s0-s5}, 80", + (0xa, 0b10, false,32) <-> "{ra, s0-s5}, -64", + (0xa, 0b10, false,64) <-> "{ra, s0-s5}, -80", + (0xa, 0b11, true, 32) <-> "{ra, s0-s5}, 80", + (0xa, 0b11, true, 64) <-> "{ra, s0-s5}, 96", + (0xa, 0b11, false,32) <-> "{ra, s0-s5}, -80", + (0xa, 0b11, false,64) <-> "{ra, s0-s5}, -96", + + (0xb, 0b00, true, 32) <-> "{ra, s0-s6}, 32", + (0xb, 0b00, true, 64) <-> "{ra, s0-s6}, 48", + (0xb, 0b00, false,32) <-> "{ra, s0-s6}, -32", + (0xb, 0b00, false,64) <-> "{ra, s0-s6}, -48", + (0xb, 0b01, true, 32) <-> "{ra, s0-s6}, 48", + (0xb, 0b01, true, 64) <-> "{ra, s0-s6}, 64", + (0xb, 0b01, false,32) <-> "{ra, s0-s6}, -48", + (0xb, 0b01, false,64) <-> "{ra, s0-s6}, -64", + (0xb, 0b10, true, 32) <-> "{ra, s0-s6}, 64", + (0xb, 0b10, true, 64) <-> "{ra, s0-s6}, 80", + (0xb, 0b10, false,32) <-> "{ra, s0-s6}, -64", + (0xb, 0b10, false,64) <-> "{ra, s0-s6}, -80", + (0xb, 0b11, true, 32) <-> "{ra, s0-s6}, 80", + (0xb, 0b11, true, 64) <-> "{ra, s0-s6}, 96", + (0xb, 0b11, false,32) <-> "{ra, s0-s6}, -80", + (0xb, 0b11, false,64) <-> "{ra, s0-s6}, -96", + + (0xc, 0b00, true, 32) <-> "{ra, s0-s7}, 48", + (0xc, 0b00, true, 64) <-> "{ra, s0-s7}, 64", + (0xc, 0b00, false,32) <-> "{ra, s0-s7}, -48", + (0xc, 0b00, false,64) <-> "{ra, s0-s7}, -64", + (0xc, 0b01, true, 32) <-> "{ra, s0-s7}, 64", + (0xc, 0b01, true, 64) <-> "{ra, s0-s7}, 80", + (0xc, 0b01, false,32) <-> "{ra, s0-s7}, -64", + (0xc, 0b01, false,64) <-> "{ra, s0-s7}, -80", + (0xc, 0b10, true, 32) <-> "{ra, s0-s7}, 80", + (0xc, 0b10, true, 64) <-> "{ra, s0-s7}, 96", + (0xc, 0b10, false,32) <-> "{ra, s0-s7}, -80", + (0xc, 0b10, false,64) <-> "{ra, s0-s7}, -96", + (0xc, 0b11, true, 32) <-> "{ra, s0-s7}, 96", + (0xc, 0b11, true, 64) <-> "{ra, s0-s7}, 112", + (0xc, 0b11, false,32) <-> "{ra, s0-s7}, -96", + (0xc, 0b11, false,64 )<-> "{ra, s0-s7}, -112", + + (0xd, 0b00, true, 32) <-> "{ra, s0-s8}, 48", + (0xd, 0b00, true, 64) <-> "{ra, s0-s8}, 64", + (0xd, 0b00, false,32) <-> "{ra, s0-s8}, -48", + (0xd, 0b00, false,64) <-> "{ra, s0-s8}, -64", + (0xd, 0b01, true, 32) <-> "{ra, s0-s8}, 64", + (0xd, 0b01, true, 64) <-> "{ra, s0-s8}, 80", + (0xd, 0b01, false,32) <-> "{ra, s0-s8}, -64", + (0xd, 0b01, false,64) <-> "{ra, s0-s8}, -80", + (0xd, 0b10, true, 32) <-> "{ra, s0-s8}, 80", + (0xd, 0b10, true, 64) <-> "{ra, s0-s8}, 96", + (0xd, 0b10, false,32) <-> "{ra, s0-s8}, -80", + (0xd, 0b10, false,64) <-> "{ra, s0-s8}, -96", + (0xd, 0b11, true, 32) <-> "{ra, s0-s8}, 96", + (0xd, 0b11, true, 64) <-> "{ra, s0-s8}, 112", + (0xd, 0b11, false,32) <-> "{ra, s0-s8}, -96", + (0xd, 0b11, false,64) <-> "{ra, s0-s8}, -112", + + (0xe, 0b00, true, 32) <-> "{ra, s0-s9}, 48", + (0xe, 0b00, true, 64) <-> "{ra, s0-s9}, 64", + (0xe, 0b00, false,32) <-> "{ra, s0-s9}, -48", + (0xe, 0b00, false,64) <-> "{ra, s0-s9}, -64", + (0xe, 0b01, true, 32) <-> "{ra, s0-s9}, 64", + (0xe, 0b01, true, 64) <-> "{ra, s0-s9}, 80", + (0xe, 0b01, false,32) <-> "{ra, s0-s9}, -64", + (0xe, 0b01, false,64) <-> "{ra, s0-s9}, -80", + (0xe, 0b10, true, 32) <-> "{ra, s0-s9}, 80", + (0xe, 0b10, true, 64) <-> "{ra, s0-s9}, 96", + (0xe, 0b10, false,32) <-> "{ra, s0-s9}, -80", + (0xe, 0b10, false,64) <-> "{ra, s0-s9}, -96", + (0xe, 0b11, true, 32) <-> "{ra, s0-s9}, 96", + (0xe, 0b11, true, 64) <-> "{ra, s0-s9}, 112", + (0xe, 0b11, false,32) <-> "{ra, s0-s9}, -96", + (0xe, 0b11, false,64) <-> "{ra, s0-s9}, -112", + + (0xf, 0b00, true, 32) <-> "{ra, s0-11}, 64", + (0xf, 0b00, true, 64) <-> "{ra, s0-11}, 80", + (0xf, 0b00, false,32) <-> "{ra, s0-11}, -64", + (0xf, 0b00, false,64) <-> "{ra, s0-11}, -80", + (0xf, 0b01, true, 32) <-> "{ra, s0-11}, 80", + (0xf, 0b01, true, 64) <-> "{ra, s0-11}, 96", + (0xf, 0b01, false,32) <-> "{ra, s0-11}, -80", + (0xf, 0b01, false,64) <-> "{ra, s0-11}, -96", + (0xf, 0b10, true, 32) <-> "{ra, s0-11}, 96", + (0xf, 0b10, true, 64) <-> "{ra, s0-11}, 112", + (0xf, 0b10, false,32) <-> "{ra, s0-11}, -96", + (0xf, 0b10, false,64) <-> "{ra, s0-11}, -112", + (0xf, 0b11, true, 32) <-> "{ra, s0-11}, 112", + (0xf, 0b11, true, 64) <-> "{ra, s0-11}, 128", + (0xf, 0b11, false,32) <-> "{ra, s0-11}, -112", + (0xf, 0b11, false,64) <-> "{ra, s0-11}, -128", } function get_stack_adj_base(rlist : bits(4)) -> int = { if(xlen == 32) then - match(rlist) { - 0b0100 => 16, - 0b0101 => 16, - 0b0110 => 16, - 0b0111 => 16, - 0b1000 => 32, - 0b1001 => 32, - 0b1010 => 32, - 0b1011 => 32, - 0b1100 => 48, - 0b1101 => 48, - 0b1110 => 48, - 0b1111 => 64, - _ => internal_error(__FILE__, __LINE__, "Unsupported rlist: " ^ bits_str(rlist)) + match rlist[3 .. 2] { + 0b01 => 16, + 0b10 => 32, + 0b11 => if rlist == 0b1111 then 64 else 48, + _ => internal_error(__FILE__, __LINE__, "Unsupported rlist: " ^ bits_str(rlist)) } else { - match(rlist) { - 0b0100 => 16, - 0b0101 => 16, - 0b0110 => 32, - 0b0111 => 32, - 0b1000 => 48, - 0b1001 => 48, - 0b1010 => 64, - 0b1011 => 64, - 0b1100 => 80, - 0b1101 => 80, - 0b1110 => 96, - 0b1111 => 112, - _ => internal_error(__FILE__, __LINE__, "Unsupported rlist: " ^ bits_str(rlist)) + match rlist[3 .. 1] { + 0b010 => 16, + 0b011 => 32, + 0b100 => 48, + 0b101 => 64, + 0b110 => 80, + 0b111 => if rlist == 0b1111 then 112 else 96, + _ => internal_error(__FILE__, __LINE__, "Unsupported rlist: " ^ bits_str(rlist)) } } } @@ -294,7 +279,7 @@ mapping spimm_to_int : bits(2) <-> int = { function zcmp_regmask(rlist : bits(4)) -> vector(32, bool) = { var mask : vector(32, bool) = undefined; - if(unsigned(rlist) >= unsigned(0b100)) then { + if rlist >=_u 0b0100 then { mask[1] = true }; @@ -316,15 +301,14 @@ function zcmp_regmask(rlist : bits(4)) -> vector(32, bool) = { } enum clause extension = Ext_Zcmp -function clause extensionEnabled(Ext_Zcmp) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_Zcd) == false & (xlen == 32 | xlen == 64) +function clause extensionEnabled(Ext_Zcmp) = extensionEnabled(Ext_Zca) & not(extensionEnabled(Ext_Zcd)) & (xlen == 32 | xlen == 64) union clause ast = CM_PUSH : (bits(4), bits(2)) mapping clause encdec_compressed = CM_PUSH(rlist, spimm) if extensionEnabled(Ext_Zcmp) <-> 0b101 @ 0b11000 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) -val process_cmpush : (bits(4), bits(2), word_width) -> Retired -function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) = { +function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) -> Retired = { let width_bytes = size_bytes(width); assert(width_bytes <= xlen_bytes); @@ -333,13 +317,12 @@ function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) = let stack_adj = negate_int(get_stack_adj_base(rlist) + spimm_int * 16); let new_sp = addr + to_bits(xlen, stack_adj); let mask = zcmp_regmask(rlist); - let bytes = if sizeof(xlen) == 32 then 4 else 8; - var imm : int = width_bytes; + var offset : int = width_bytes; foreach (i from 31 downto 1) { if mask[i] then { - match ext_data_get_addr(sp, to_bits(xlen, negate_int(imm)), Write(Data), xlen / 8) { + match ext_data_get_addr(sp, to_bits(xlen, negate_int(offset)), Write(Data), xlen / 8) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -353,7 +336,7 @@ function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) = MemValue(_) => { let reg_val = X(to_bits(5, i)); match mem_write_value(paddr, width_bytes, reg_val[width_bytes * 8 - 1 .. 0], false, false, false) { - MemValue(true) => { imm = imm + width_bytes }, + MemValue(true) => { offset = offset + width_bytes }, MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } @@ -376,10 +359,10 @@ function clause execute (CM_PUSH(rlist, spimm)) = { } mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 32) <-> - "cm.push" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, false, true) if (sizeof(xlen) == 32) + "cm.push" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, false, 32) if (sizeof(xlen) == 32) mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 64) <-> - "cm.push" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, false, false) if (sizeof(xlen) == 64) + "cm.push" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, false, 64) if (sizeof(xlen) == 64) union clause ast = CM_POP : (bits(4), bits(2)) @@ -387,8 +370,7 @@ union clause ast = CM_POP : (bits(4), bits(2)) mapping clause encdec_compressed = CM_POP(rlist, spimm) if extensionEnabled(Ext_Zcmp) <-> 0b101 @ 0b11010 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) -val process_cmpop : (bits(4), bits(2), word_width, bool, bool) -> Retired -function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, write_pc : bool, write_a0 : bool) = { +function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, write_pc : bool, write_a0 : bool) -> Retired = { let width_bytes = size_bytes(width); assert(width_bytes <= xlen_bytes); @@ -401,11 +383,11 @@ function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, wr X(sp) = new_sp; - var imm : int = width_bytes; + var offset : int = width_bytes; foreach (i from 31 downto 1) { if mask[i] then { - match ext_data_get_addr(sp, to_bits(xlen, negate_int(imm)), Write(Data), xlen / 8) { + match ext_data_get_addr(sp, to_bits(xlen, negate_int(offset)), Write(Data), xlen / 8) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -417,7 +399,7 @@ function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, wr MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, MemValue(v) => { X(to_bits(5, i)) = extend_value(true, v); - imm = imm + width_bytes + offset = offset + width_bytes } } } @@ -428,14 +410,12 @@ function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, wr // cm.popret write pc with ra. if write_pc then { - let ra_val = X(to_bits(5, 1)); - set_next_pc(ra_val); + set_next_pc(X(0b00001)); }; // cm.popretz write a0 with zero. if write_a0 then { - let a0 : regidx = to_bits(5, 10); - X(a0) = to_bits(xlen, 0); + X(0b01010) = zeros(); }; RETIRE_SUCCESS @@ -449,10 +429,10 @@ function clause execute (CM_POP(rlist, spimm)) = { } mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 32) <-> - "cm.pop" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, true) if (sizeof(xlen) == 32) + "cm.pop" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, 32) if (sizeof(xlen) == 32) mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 64) <-> - "cm.pop" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, false) if (sizeof(xlen) == 64) + "cm.pop" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, 64) if (sizeof(xlen) == 64) union clause ast = CM_POPRET : (bits(4), bits(2)) @@ -468,10 +448,10 @@ function clause execute (CM_POPRET(rlist, spimm)) = { } mapping clause assembly = CM_POPRET(rlist, spimm) if (sizeof(xlen) == 32) <-> - "cm.popret" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, true) if (sizeof(xlen) == 32) + "cm.popret" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, 32) if (sizeof(xlen) == 32) mapping clause assembly = CM_POPRET(rlist, spimm) if (sizeof(xlen) == 64) <-> - "cm.popret" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, false) if (sizeof(xlen) == 64) + "cm.popret" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, 64) if (sizeof(xlen) == 64) union clause ast = CM_POPRETZ : (bits(4), bits(2)) @@ -485,3 +465,62 @@ function clause execute (CM_POPRETZ(rlist, spimm)) = { else process_cmpop(rlist, spimm, DOUBLE, false, true) } + +mapping clause assembly = CM_POPRETZ(rlist, spimm) if (sizeof(xlen) == 32) <-> + "cm.popretz" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, 32) if (sizeof(xlen) == 32) + +mapping clause assembly = CM_POPRETZ(rlist, spimm) if (sizeof(xlen) == 64) <-> + "cm.popretz" ^ spc() ^ zcmp_assembly_mapping(rlist, spimm, true, 64) if (sizeof(xlen) == 64) + +// Differ from creg_name. +mapping rns_name : cregidx <-> string = { + 0b000 <-> "s0", + 0b001 <-> "s1", + 0b010 <-> "s2", + 0b011 <-> "s3", + 0b100 <-> "s4", + 0b101 <-> "s5", + 0b110 <-> "s6", + 0b111 <-> "s7", +} + +mapping rns_to_regidx : cregidx <-> regidx = { + 0b000 <-> 0b01000, + 0b001 <-> 0b01001, + 0b010 <-> 0b10010, + 0b011 <-> 0b10011, + 0b100 <-> 0b10100, + 0b101 <-> 0b10101, + 0b110 <-> 0b10110, + 0b111 <-> 0b10111, +} + +union clause ast = CM_MVA01S : (cregidx, cregidx) + +mapping clause encdec_compressed = CM_MVA01S(r1s', r2s') if extensionEnabled(Ext_Zcmp) + <-> 0b101 @ 0b011 @ r1s' : cregidx @ 0b11 @ r2s' : cregidx @ 0b10 if extensionEnabled(Ext_Zcmp) + +function clause execute (CM_MVA01S(r1s', r2s')) = { + X(0b01010) = X(rns_to_regidx(r1s')); + X(0b01011) = X(rns_to_regidx(r2s')); + + RETIRE_SUCCESS +} + +mapping clause assembly = CM_MVA01S(r1s', r2s') <-> + "cm.mva01s" ^ spc() ^ rns_name(r1s') ^ sep() ^ rns_name(r2s') + +union clause ast = CM_MVSA01 : (cregidx, cregidx) + +mapping clause encdec_compressed = CM_MVSA01(r1s', r2s') if extensionEnabled(Ext_Zcmp) + <-> 0b101 @ 0b011 @ r1s' : cregidx @ 0b01 @ r2s' : cregidx @ 0b10 if extensionEnabled(Ext_Zcmp) + +function clause execute (CM_MVSA01(r1s', r2s')) = { + X(rns_to_regidx(r1s')) = X(0b01010); + X(rns_to_regidx(r2s')) = X(0b01011); + + RETIRE_SUCCESS +} + +mapping clause assembly = CM_MVSA01(r1s', r2s') <-> + "cm.mvsa01" ^ spc() ^ rns_name(r1s') ^ sep() ^ rns_name(r2s') From eb470182cc5b8bc9bde5284539a4447e6c91e7c8 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Fri, 8 Nov 2024 00:34:30 +0800 Subject: [PATCH 9/9] Refactor code to conform to community standards --- model/riscv_insts_zcmp.sail | 511 +++++++++++++++++------------------- 1 file changed, 238 insertions(+), 273 deletions(-) diff --git a/model/riscv_insts_zcmp.sail b/model/riscv_insts_zcmp.sail index 4609ebff0..4e5eca6f4 100644 --- a/model/riscv_insts_zcmp.sail +++ b/model/riscv_insts_zcmp.sail @@ -9,209 +9,209 @@ // first bool represent the stack_adi is positive or negative. // second bool represent xlen is 32 or 64. mapping zcmp_assembly_mapping : (bits(4), bits(2), bool, {32, 64}) <-> string = { - (0x4, 0b00, true, 32) <-> "{ra}, 16", - (0x4, 0b00, true, 64) <-> "{ra}, 32", - (0x4, 0b00, false,32) <-> "{ra}, -16", - (0x4, 0b00, false,64) <-> "{ra}, -32", - (0x4, 0b01, true, 32) <-> "{ra}, 32", - (0x4, 0b01, true, 64) <-> "{ra}, 48", - (0x4, 0b01, false,32) <-> "{ra}, -32", - (0x4, 0b01, false,64) <-> "{ra}, -48", - (0x4, 0b10, true, 32) <-> "{ra}, 48", - (0x4, 0b10, true, 64) <-> "{ra}, 64", - (0x4, 0b10, false,32) <-> "{ra}, -48", - (0x4, 0b10, false,64) <-> "{ra}, -64", - (0x4, 0b11, true, 32) <-> "{ra}, 64", - (0x4, 0b11, true, 64) <-> "{ra}, 80", - (0x4, 0b11, false,32) <-> "{ra}, -64", - (0x4, 0b11, false,64) <-> "{ra}, -80", - - (0x5, 0b00, true, 32) <-> "{ra, s0}, 16", - (0x5, 0b00, true, 64) <-> "{ra, s0}, 32", - (0x5, 0b00, false,32) <-> "{ra, s0}, -16", - (0x5, 0b00, false,64) <-> "{ra, s0}, -32", - (0x5, 0b01, true, 32) <-> "{ra, s0}, 32", - (0x5, 0b01, true, 64) <-> "{ra, s0}, 48", - (0x5, 0b01, false,32) <-> "{ra, s0}, -32", - (0x5, 0b01, false,64) <-> "{ra, s0}, -48", - (0x5, 0b10, true, 32) <-> "{ra, s0}, 48", - (0x5, 0b10, true, 64) <-> "{ra, s0}, 64", - (0x5, 0b10, false,32) <-> "{ra, s0}, -48", - (0x5, 0b10, false,64) <-> "{ra, s0}, -64", - (0x5, 0b11, true, 32) <-> "{ra, s0}, 64", - (0x5, 0b11, true, 64) <-> "{ra, s0}, 80", - (0x5, 0b11, false,32) <-> "{ra, s0}, -64", - (0x5, 0b11, false,64) <-> "{ra, s0}, -80", - - (0x6, 0b00, true, 32) <-> "{ra, s0-s1}, -16", - (0x6, 0b00, true, 64) <-> "{ra, s0-s1}, -32", - (0x6, 0b00, false,32) <-> "{ra, s0-s1}, --16", - (0x6, 0b00, false,64) <-> "{ra, s0-s1}, --32", - (0x6, 0b01, true, 32) <-> "{ra, s0-s1}, -32", - (0x6, 0b01, true, 64) <-> "{ra, s0-s1}, -48", - (0x6, 0b01, false,32) <-> "{ra, s0-s1}, --32", - (0x6, 0b01, false,64) <-> "{ra, s0-s1}, --48", - (0x6, 0b10, true, 32) <-> "{ra, s0-s1}, -48", - (0x6, 0b10, true, 64) <-> "{ra, s0-s1}, -64", - (0x6, 0b10, false,32) <-> "{ra, s0-s1}, --48", - (0x6, 0b10, false,64) <-> "{ra, s0-s1}, --64", - (0x6, 0b11, true, 32) <-> "{ra, s0-s1}, -64", - (0x6, 0b11, true, 64) <-> "{ra, s0-s1}, -80", - (0x6, 0b11, false,32) <-> "{ra, s0-s1}, --64", - (0x6, 0b11, false,64) <-> "{ra, s0-s1}, --80", - - (0x7, 0b00, true, 32) <-> "{ra, s0-s2}, 16", - (0x7, 0b00, true, 64) <-> "{ra, s0-s2}, 32", - (0x7, 0b00, false,32) <-> "{ra, s0-s2}, -16", - (0x7, 0b00, false,64) <-> "{ra, s0-s2}, -32", - (0x7, 0b01, true, 32) <-> "{ra, s0-s2}, 32", - (0x7, 0b01, true, 64) <-> "{ra, s0-s2}, 48", - (0x7, 0b01, false,32) <-> "{ra, s0-s2}, -32", - (0x7, 0b01, false,64) <-> "{ra, s0-s2}, -48", - (0x7, 0b10, true, 32) <-> "{ra, s0-s2}, 48", - (0x7, 0b10, true, 64) <-> "{ra, s0-s2}, 64", - (0x7, 0b10, false,32) <-> "{ra, s0-s2}, -48", - (0x7, 0b10, false,64) <-> "{ra, s0-s2}, -64", - (0x7, 0b11, true, 32) <-> "{ra, s0-s2}, 64", - (0x7, 0b11, true, 64) <-> "{ra, s0-s2}, 80", - (0x7, 0b11, false,32) <-> "{ra, s0-s2}, -64", - (0x7, 0b11, false,64) <-> "{ra, s0-s2}, -80", - - (0x8, 0b00, true, 32) <-> "{ra, s0-s3}, 32", - (0x8, 0b00, true, 64) <-> "{ra, s0-s3}, 48", - (0x8, 0b00, false,32) <-> "{ra, s0-s3}, -32", - (0x8, 0b00, false,64) <-> "{ra, s0-s3}, -48", - (0x8, 0b01, true, 32) <-> "{ra, s0-s3}, 48", - (0x8, 0b01, true, 64) <-> "{ra, s0-s3}, 64", - (0x8, 0b01, false,32) <-> "{ra, s0-s3}, -48", - (0x8, 0b01, false,64) <-> "{ra, s0-s3}, -64", - (0x8, 0b10, true, 32) <-> "{ra, s0-s3}, 64", - (0x8, 0b10, true, 64) <-> "{ra, s0-s3}, 80", - (0x8, 0b10, false,32) <-> "{ra, s0-s3}, -64", - (0x8, 0b10, false,64) <-> "{ra, s0-s3}, -80", - (0x8, 0b11, true, 32) <-> "{ra, s0-s3}, 80", - (0x8, 0b11, true, 64) <-> "{ra, s0-s3}, 96", - (0x8, 0b11, false,32) <-> "{ra, s0-s3}, -80", - (0x8, 0b11, false,64) <-> "{ra, s0-s3}, -96", - - (0x9, 0b00, true, 32) <-> "{ra, s0-s4}, 32", - (0x9, 0b00, true, 64) <-> "{ra, s0-s4}, 48", - (0x9, 0b00, false,32) <-> "{ra, s0-s4}, -32", - (0x9, 0b00, false,64) <-> "{ra, s0-s4}, -48", - (0x9, 0b01, true, 32) <-> "{ra, s0-s4}, 48", - (0x9, 0b01, true, 64) <-> "{ra, s0-s4}, 64", - (0x9, 0b01, false,32) <-> "{ra, s0-s4}, -48", - (0x9, 0b01, false,64) <-> "{ra, s0-s4}, -64", - (0x9, 0b10, true, 32) <-> "{ra, s0-s4}, 64", - (0x9, 0b10, true, 64) <-> "{ra, s0-s4}, 80", - (0x9, 0b10, false,32) <-> "{ra, s0-s4}, -64", - (0x9, 0b10, false,64) <-> "{ra, s0-s4}, -80", - (0x9, 0b11, true, 32) <-> "{ra, s0-s4}, 80", - (0x9, 0b11, true, 64) <-> "{ra, s0-s4}, 96", - (0x9, 0b11, false,32) <-> "{ra, s0-s4}, -80", - (0x9, 0b11, false,64) <-> "{ra, s0-s4}, -96", - - (0xa, 0b00, true, 32) <-> "{ra, s0-s5}, 32", - (0xa, 0b00, true, 64) <-> "{ra, s0-s5}, 48", - (0xa, 0b00, false,32) <-> "{ra, s0-s5}, -32", - (0xa, 0b00, false,64) <-> "{ra, s0-s5}, -48", - (0xa, 0b01, true, 32) <-> "{ra, s0-s5}, 48", - (0xa, 0b01, true, 64) <-> "{ra, s0-s5}, 64", - (0xa, 0b01, false,32) <-> "{ra, s0-s5}, -48", - (0xa, 0b01, false,64) <-> "{ra, s0-s5}, -64", - (0xa, 0b10, true, 32) <-> "{ra, s0-s5}, 64", - (0xa, 0b10, true, 64) <-> "{ra, s0-s5}, 80", - (0xa, 0b10, false,32) <-> "{ra, s0-s5}, -64", - (0xa, 0b10, false,64) <-> "{ra, s0-s5}, -80", - (0xa, 0b11, true, 32) <-> "{ra, s0-s5}, 80", - (0xa, 0b11, true, 64) <-> "{ra, s0-s5}, 96", - (0xa, 0b11, false,32) <-> "{ra, s0-s5}, -80", - (0xa, 0b11, false,64) <-> "{ra, s0-s5}, -96", - - (0xb, 0b00, true, 32) <-> "{ra, s0-s6}, 32", - (0xb, 0b00, true, 64) <-> "{ra, s0-s6}, 48", - (0xb, 0b00, false,32) <-> "{ra, s0-s6}, -32", - (0xb, 0b00, false,64) <-> "{ra, s0-s6}, -48", - (0xb, 0b01, true, 32) <-> "{ra, s0-s6}, 48", - (0xb, 0b01, true, 64) <-> "{ra, s0-s6}, 64", - (0xb, 0b01, false,32) <-> "{ra, s0-s6}, -48", - (0xb, 0b01, false,64) <-> "{ra, s0-s6}, -64", - (0xb, 0b10, true, 32) <-> "{ra, s0-s6}, 64", - (0xb, 0b10, true, 64) <-> "{ra, s0-s6}, 80", - (0xb, 0b10, false,32) <-> "{ra, s0-s6}, -64", - (0xb, 0b10, false,64) <-> "{ra, s0-s6}, -80", - (0xb, 0b11, true, 32) <-> "{ra, s0-s6}, 80", - (0xb, 0b11, true, 64) <-> "{ra, s0-s6}, 96", - (0xb, 0b11, false,32) <-> "{ra, s0-s6}, -80", - (0xb, 0b11, false,64) <-> "{ra, s0-s6}, -96", - - (0xc, 0b00, true, 32) <-> "{ra, s0-s7}, 48", - (0xc, 0b00, true, 64) <-> "{ra, s0-s7}, 64", - (0xc, 0b00, false,32) <-> "{ra, s0-s7}, -48", - (0xc, 0b00, false,64) <-> "{ra, s0-s7}, -64", - (0xc, 0b01, true, 32) <-> "{ra, s0-s7}, 64", - (0xc, 0b01, true, 64) <-> "{ra, s0-s7}, 80", - (0xc, 0b01, false,32) <-> "{ra, s0-s7}, -64", - (0xc, 0b01, false,64) <-> "{ra, s0-s7}, -80", - (0xc, 0b10, true, 32) <-> "{ra, s0-s7}, 80", - (0xc, 0b10, true, 64) <-> "{ra, s0-s7}, 96", - (0xc, 0b10, false,32) <-> "{ra, s0-s7}, -80", - (0xc, 0b10, false,64) <-> "{ra, s0-s7}, -96", - (0xc, 0b11, true, 32) <-> "{ra, s0-s7}, 96", - (0xc, 0b11, true, 64) <-> "{ra, s0-s7}, 112", - (0xc, 0b11, false,32) <-> "{ra, s0-s7}, -96", - (0xc, 0b11, false,64 )<-> "{ra, s0-s7}, -112", - - (0xd, 0b00, true, 32) <-> "{ra, s0-s8}, 48", - (0xd, 0b00, true, 64) <-> "{ra, s0-s8}, 64", - (0xd, 0b00, false,32) <-> "{ra, s0-s8}, -48", - (0xd, 0b00, false,64) <-> "{ra, s0-s8}, -64", - (0xd, 0b01, true, 32) <-> "{ra, s0-s8}, 64", - (0xd, 0b01, true, 64) <-> "{ra, s0-s8}, 80", - (0xd, 0b01, false,32) <-> "{ra, s0-s8}, -64", - (0xd, 0b01, false,64) <-> "{ra, s0-s8}, -80", - (0xd, 0b10, true, 32) <-> "{ra, s0-s8}, 80", - (0xd, 0b10, true, 64) <-> "{ra, s0-s8}, 96", - (0xd, 0b10, false,32) <-> "{ra, s0-s8}, -80", - (0xd, 0b10, false,64) <-> "{ra, s0-s8}, -96", - (0xd, 0b11, true, 32) <-> "{ra, s0-s8}, 96", - (0xd, 0b11, true, 64) <-> "{ra, s0-s8}, 112", - (0xd, 0b11, false,32) <-> "{ra, s0-s8}, -96", - (0xd, 0b11, false,64) <-> "{ra, s0-s8}, -112", - - (0xe, 0b00, true, 32) <-> "{ra, s0-s9}, 48", - (0xe, 0b00, true, 64) <-> "{ra, s0-s9}, 64", - (0xe, 0b00, false,32) <-> "{ra, s0-s9}, -48", - (0xe, 0b00, false,64) <-> "{ra, s0-s9}, -64", - (0xe, 0b01, true, 32) <-> "{ra, s0-s9}, 64", - (0xe, 0b01, true, 64) <-> "{ra, s0-s9}, 80", - (0xe, 0b01, false,32) <-> "{ra, s0-s9}, -64", - (0xe, 0b01, false,64) <-> "{ra, s0-s9}, -80", - (0xe, 0b10, true, 32) <-> "{ra, s0-s9}, 80", - (0xe, 0b10, true, 64) <-> "{ra, s0-s9}, 96", - (0xe, 0b10, false,32) <-> "{ra, s0-s9}, -80", - (0xe, 0b10, false,64) <-> "{ra, s0-s9}, -96", - (0xe, 0b11, true, 32) <-> "{ra, s0-s9}, 96", - (0xe, 0b11, true, 64) <-> "{ra, s0-s9}, 112", - (0xe, 0b11, false,32) <-> "{ra, s0-s9}, -96", - (0xe, 0b11, false,64) <-> "{ra, s0-s9}, -112", - - (0xf, 0b00, true, 32) <-> "{ra, s0-11}, 64", - (0xf, 0b00, true, 64) <-> "{ra, s0-11}, 80", - (0xf, 0b00, false,32) <-> "{ra, s0-11}, -64", - (0xf, 0b00, false,64) <-> "{ra, s0-11}, -80", - (0xf, 0b01, true, 32) <-> "{ra, s0-11}, 80", - (0xf, 0b01, true, 64) <-> "{ra, s0-11}, 96", - (0xf, 0b01, false,32) <-> "{ra, s0-11}, -80", - (0xf, 0b01, false,64) <-> "{ra, s0-11}, -96", - (0xf, 0b10, true, 32) <-> "{ra, s0-11}, 96", - (0xf, 0b10, true, 64) <-> "{ra, s0-11}, 112", - (0xf, 0b10, false,32) <-> "{ra, s0-11}, -96", - (0xf, 0b10, false,64) <-> "{ra, s0-11}, -112", - (0xf, 0b11, true, 32) <-> "{ra, s0-11}, 112", - (0xf, 0b11, true, 64) <-> "{ra, s0-11}, 128", - (0xf, 0b11, false,32) <-> "{ra, s0-11}, -112", - (0xf, 0b11, false,64) <-> "{ra, s0-11}, -128", + (0x4, 0b00, true, 32) <-> "{ra} " ^ sep() ^ "16", + (0x4, 0b00, true, 64) <-> "{ra} " ^ sep() ^ "32", + (0x4, 0b00, false,32) <-> "{ra} " ^ sep() ^ "-16", + (0x4, 0b00, false,64) <-> "{ra} " ^ sep() ^ "-32", + (0x4, 0b01, true, 32) <-> "{ra} " ^ sep() ^ "32", + (0x4, 0b01, true, 64) <-> "{ra} " ^ sep() ^ "48", + (0x4, 0b01, false,32) <-> "{ra} " ^ sep() ^ "-32", + (0x4, 0b01, false,64) <-> "{ra} " ^ sep() ^ "-48", + (0x4, 0b10, true, 32) <-> "{ra} " ^ sep() ^ "48", + (0x4, 0b10, true, 64) <-> "{ra} " ^ sep() ^ "64", + (0x4, 0b10, false,32) <-> "{ra} " ^ sep() ^ "-48", + (0x4, 0b10, false,64) <-> "{ra} " ^ sep() ^ "-64", + (0x4, 0b11, true, 32) <-> "{ra} " ^ sep() ^ "64", + (0x4, 0b11, true, 64) <-> "{ra} " ^ sep() ^ "80", + (0x4, 0b11, false,32) <-> "{ra} " ^ sep() ^ "-64", + (0x4, 0b11, false,64) <-> "{ra} " ^ sep() ^ "-80", + + (0x5, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "16", + (0x5, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "32", + (0x5, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-16", + (0x5, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-32", + (0x5, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "32", + (0x5, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "48", + (0x5, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-32", + (0x5, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-48", + (0x5, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "48", + (0x5, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "64", + (0x5, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-48", + (0x5, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-64", + (0x5, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "64", + (0x5, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "80", + (0x5, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-64", + (0x5, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0}" ^ sep() ^ "-80", + + (0x6, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-16", + (0x6, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-32", + (0x6, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--16", + (0x6, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--32", + (0x6, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-32", + (0x6, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-48", + (0x6, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--32", + (0x6, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--48", + (0x6, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-48", + (0x6, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-64", + (0x6, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--48", + (0x6, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--64", + (0x6, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-64", + (0x6, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "-80", + (0x6, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--64", + (0x6, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s1}" ^ sep() ^ "--80", + + (0x7, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "16", + (0x7, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "32", + (0x7, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-16", + (0x7, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-32", + (0x7, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "32", + (0x7, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "48", + (0x7, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-32", + (0x7, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-48", + (0x7, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "48", + (0x7, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "64", + (0x7, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-48", + (0x7, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-64", + (0x7, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "64", + (0x7, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "80", + (0x7, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-64", + (0x7, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s2}" ^ sep() ^ "-80", + + (0x8, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "32", + (0x8, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "48", + (0x8, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-32", + (0x8, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-48", + (0x8, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "48", + (0x8, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "64", + (0x8, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-48", + (0x8, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-64", + (0x8, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "64", + (0x8, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "80", + (0x8, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-64", + (0x8, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-80", + (0x8, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "80", + (0x8, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "96", + (0x8, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-80", + (0x8, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s3}" ^ sep() ^ "-96", + + (0x9, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "32", + (0x9, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "48", + (0x9, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-32", + (0x9, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-48", + (0x9, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "48", + (0x9, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "64", + (0x9, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-48", + (0x9, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-64", + (0x9, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "64", + (0x9, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "80", + (0x9, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-64", + (0x9, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-80", + (0x9, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "80", + (0x9, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "96", + (0x9, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-80", + (0x9, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s4}" ^ sep() ^ "-96", + + (0xa, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "32", + (0xa, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "48", + (0xa, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-32", + (0xa, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-48", + (0xa, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "48", + (0xa, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "64", + (0xa, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-48", + (0xa, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-64", + (0xa, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "64", + (0xa, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "80", + (0xa, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-64", + (0xa, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-80", + (0xa, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "80", + (0xa, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "96", + (0xa, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-80", + (0xa, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s5} " ^ sep() ^ "-96", + + (0xb, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "32", + (0xb, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "48", + (0xb, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-32", + (0xb, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-48", + (0xb, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "48", + (0xb, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "64", + (0xb, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-48", + (0xb, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-64", + (0xb, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "64", + (0xb, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "80", + (0xb, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-64", + (0xb, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-80", + (0xb, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "80", + (0xb, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "96", + (0xb, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-80", + (0xb, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s6}" ^ sep() ^ "-96", + + (0xc, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "48", + (0xc, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "64", + (0xc, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-48", + (0xc, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-64", + (0xc, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "64", + (0xc, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "80", + (0xc, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-64", + (0xc, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-80", + (0xc, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "80", + (0xc, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "96", + (0xc, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-80", + (0xc, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-96", + (0xc, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "96", + (0xc, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "112", + (0xc, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-96", + (0xc, 0b11, false,64 )<-> "{ra" ^ sep() ^ "s0-s7}" ^ sep() ^ "-112", + + (0xd, 0b00, true, 32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "48", + (0xd, 0b00, true, 64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "64", + (0xd, 0b00, false,32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-48", + (0xd, 0b00, false,64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-64", + (0xd, 0b01, true, 32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "64", + (0xd, 0b01, true, 64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "80", + (0xd, 0b01, false,32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-64", + (0xd, 0b01, false,64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-80", + (0xd, 0b10, true, 32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "80", + (0xd, 0b10, true, 64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "96", + (0xd, 0b10, false,32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-80", + (0xd, 0b10, false,64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-96", + (0xd, 0b11, true, 32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "96", + (0xd, 0b11, true, 64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "112", + (0xd, 0b11, false,32) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-96", + (0xd, 0b11, false,64) <-> "{ra" ^ sep() ^ " s0-s8}" ^ sep() ^ "-112", + + (0xe, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "48", + (0xe, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "64", + (0xe, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-48", + (0xe, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-64", + (0xe, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "64", + (0xe, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "80", + (0xe, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-64", + (0xe, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-80", + (0xe, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "80", + (0xe, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "96", + (0xe, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-80", + (0xe, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-96", + (0xe, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "96", + (0xe, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "112", + (0xe, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-96", + (0xe, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-s9}" ^ sep() ^ "-112", + + (0xf, 0b00, true, 32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "64", + (0xf, 0b00, true, 64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "80", + (0xf, 0b00, false,32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-64", + (0xf, 0b00, false,64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-80", + (0xf, 0b01, true, 32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "80", + (0xf, 0b01, true, 64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "96", + (0xf, 0b01, false,32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-80", + (0xf, 0b01, false,64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-96", + (0xf, 0b10, true, 32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "96", + (0xf, 0b10, true, 64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "112", + (0xf, 0b10, false,32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-96", + (0xf, 0b10, false,64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-112", + (0xf, 0b11, true, 32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "112", + (0xf, 0b11, true, 64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "128", + (0xf, 0b11, false,32) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-112", + (0xf, 0b11, false,64) <-> "{ra" ^ sep() ^ "s0-11}" ^ sep() ^ "-128", } function get_stack_adj_base(rlist : bits(4)) -> int = { @@ -235,67 +235,24 @@ function get_stack_adj_base(rlist : bits(4)) -> int = { } } -mapping reg_list : bits(4) <-> string = { - 0b0100 <-> "ra", - 0b0101 <-> "ra, s0", - 0b0110 <-> "ra, s0-s1", - 0b0111 <-> "ra, s0-s2", - 0b1000 <-> "ra, s0-s3", - 0b1001 <-> "ra, s0-s4", - 0b1010 <-> "ra, s0-s5", - 0b1011 <-> "ra, s0-s6", - 0b1100 <-> "ra, s0-s7", - 0b1101 <-> "ra, s0-s8", - 0b1110 <-> "ra, s0-s9", - 0b1111 <-> "ra, s0-s11", -} - -mapping rlist_to_int : bits(4) <-> int = { - 0b0000 <-> 0, - 0b0001 <-> 1, - 0b0010 <-> 2, - 0b0011 <-> 3, - 0b0100 <-> 4, - 0b0101 <-> 5, - 0b0110 <-> 6, - 0b0111 <-> 7, - 0b1000 <-> 8, - 0b1001 <-> 9, - 0b1010 <-> 10, - 0b1011 <-> 11, - 0b1100 <-> 12, - 0b1101 <-> 13, - 0b1110 <-> 14, - 0b1111 <-> 15, -} - -mapping spimm_to_int : bits(2) <-> int = { - 0b00 <-> 0, - 0b01 <-> 1, - 0b10 <-> 2, - 0b11 <-> 3, -} - -function zcmp_regmask(rlist : bits(4)) -> vector(32, bool) = { - var mask : vector(32, bool) = undefined; +function zcmp_regmask(rlist : bits(4)) -> bits(32) = { + var mask : bits(32) = zeros(); if rlist >=_u 0b0100 then { - mask[1] = true + mask[1] = bitone }; - let rlist_num = rlist_to_int(rlist); - - foreach (i from 5 to rlist_num) { + foreach (i from 5 to unsigned(rlist)) { assert(i <= 15); if( (i - 5) < 2 ) then - mask[3 + i] = true + mask[3 + i] = bitone else { - mask[11 + i] = true + mask[11 + i] = bitone }; }; if(rlist == zero_extend(0xf)) then - mask[27] = true; + mask[27] = bitone; mask } @@ -308,24 +265,23 @@ union clause ast = CM_PUSH : (bits(4), bits(2)) mapping clause encdec_compressed = CM_PUSH(rlist, spimm) if extensionEnabled(Ext_Zcmp) <-> 0b101 @ 0b11000 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) -function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) -> Retired = { - let width_bytes = size_bytes(width); +function process_cmpush (rlist : bits(4), spimm : bits(2)) -> Retired = { + let width_bytes = xlen_bytes; assert(width_bytes <= xlen_bytes); let addr = X(sp); - let spimm_int = spimm_to_int(spimm); - let stack_adj = negate_int(get_stack_adj_base(rlist) + spimm_int * 16); + let stack_adj = negate_int(get_stack_adj_base(rlist) + unsigned(spimm) * 16); let new_sp = addr + to_bits(xlen, stack_adj); let mask = zcmp_regmask(rlist); var offset : int = width_bytes; foreach (i from 31 downto 1) { - if mask[i] then { + if mask[i] == bitone then { match ext_data_get_addr(sp, to_bits(xlen, negate_int(offset)), Write(Data), xlen / 8) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width) + if check_misaligned(vaddr, size_bytes(xlen_bytes)) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -352,10 +308,12 @@ function process_cmpush (rlist : bits(4), spimm : bits(2), width : word_width) - } function clause execute (CM_PUSH(rlist, spimm)) = { + assert(rlist >=_u 0b0100); + if (xlen == 32) then - process_cmpush(rlist, spimm, WORD) + process_cmpush(rlist, spimm) else - process_cmpush(rlist, spimm, DOUBLE) + process_cmpush(rlist, spimm) } mapping clause assembly = CM_PUSH(rlist, spimm) if (sizeof(xlen) == 32) <-> @@ -370,13 +328,12 @@ union clause ast = CM_POP : (bits(4), bits(2)) mapping clause encdec_compressed = CM_POP(rlist, spimm) if extensionEnabled(Ext_Zcmp) <-> 0b101 @ 0b11010 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) -function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, write_pc : bool, write_a0 : bool) -> Retired = { - let width_bytes = size_bytes(width); +function process_cmpop (rlist : bits(4), spimm : bits(2), write_pc : bool, write_a0 : bool) -> Retired = { + let width_bytes = xlen_bytes; assert(width_bytes <= xlen_bytes); let addr = X(sp); - let spimm_int = spimm_to_int(spimm); - let stack_adj = get_stack_adj_base(rlist) + spimm_int * 16; + let stack_adj = get_stack_adj_base(rlist) + unsigned(spimm) * 16; let new_sp = addr + to_bits(xlen, stack_adj); let mask = zcmp_regmask(rlist); let bytes = if sizeof(xlen) == 32 then 4 else 8; @@ -386,11 +343,11 @@ function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, wr var offset : int = width_bytes; foreach (i from 31 downto 1) { - if mask[i] then { + if mask[i] == bitone then { match ext_data_get_addr(sp, to_bits(xlen, negate_int(offset)), Write(Data), xlen / 8) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width) + if check_misaligned(vaddr, size_bytes(xlen_bytes)) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -422,10 +379,12 @@ function process_cmpop (rlist : bits(4), spimm : bits(2), width : word_width, wr } function clause execute (CM_POP(rlist, spimm)) = { + assert(rlist >=_u 0b0100); + if (xlen == 32) then - process_cmpop(rlist, spimm, WORD, false, false) + process_cmpop(rlist, spimm, false, false) else - process_cmpop(rlist, spimm, DOUBLE, false, false) + process_cmpop(rlist, spimm, false, false) } mapping clause assembly = CM_POP(rlist, spimm) if (sizeof(xlen) == 32) <-> @@ -441,10 +400,12 @@ mapping clause encdec_compressed = CM_POPRET(rlist, spimm) if extensionEnabled <-> 0b101 @ 0b11110 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) function clause execute (CM_POPRET(rlist, spimm)) = { + assert(rlist >=_u 0b0100); + if (xlen == 32) then - process_cmpop(rlist, spimm, WORD, true, false) + process_cmpop(rlist, spimm, true, false) else - process_cmpop(rlist, spimm, DOUBLE, true, false) + process_cmpop(rlist, spimm, true, false) } mapping clause assembly = CM_POPRET(rlist, spimm) if (sizeof(xlen) == 32) <-> @@ -460,10 +421,12 @@ mapping clause encdec_compressed = CM_POPRETZ(rlist, spimm) if extensionEnable <-> 0b101 @ 0b11100 @ rlist : bits(4) @ spimm : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) function clause execute (CM_POPRETZ(rlist, spimm)) = { + assert(rlist >=_u 0b0100); + if (xlen == 32) then - process_cmpop(rlist, spimm, WORD, false, true) + process_cmpop(rlist, spimm, false, true) else - process_cmpop(rlist, spimm, DOUBLE, false, true) + process_cmpop(rlist, spimm, false, true) } mapping clause assembly = CM_POPRETZ(rlist, spimm) if (sizeof(xlen) == 32) <-> @@ -516,6 +479,8 @@ mapping clause encdec_compressed = CM_MVSA01(r1s', r2s') if extensionEnabled(E <-> 0b101 @ 0b011 @ r1s' : cregidx @ 0b01 @ r2s' : cregidx @ 0b10 if extensionEnabled(Ext_Zcmp) function clause execute (CM_MVSA01(r1s', r2s')) = { + assert(r1s' != r2s'); + X(rns_to_regidx(r1s')) = X(0b01010); X(rns_to_regidx(r2s')) = X(0b01011);