From 79fc5ad33a2215497f080aeabe40a659fa38e0fe Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur <103736+pmundkur@users.noreply.github.com> Date: Mon, 24 Feb 2025 15:41:51 -0600 Subject: [PATCH 1/3] Refactor instruction retirement. The eventual goal here is to surface wait-states of the hart (e.g. as caused by WFI and WRS.{NTO,STO}) into the stepper, and handle debug triggers from execution for extensions such as Sdtrig. The refactor makes interrupt and exception handling more symmetrical: both are now handled in the stepper. This also removes the model-internal global instbits register into a stepper-local variable, which fixes #412. This refactor is based on ideas discussed in #398 and #412. Co-authored-by: Tim Hutt Co-authored-by: Jessica Clarke Co-authored-by: Alasdair Armstrong --- Makefile.old | 3 +- model/CMakeLists.txt | 1 + model/riscv_inst_retire.sail | 28 ++++ model/riscv_insts_aext.sail | 30 ++-- model/riscv_insts_base.sail | 66 ++++---- model/riscv_insts_begin.sail | 2 +- model/riscv_insts_dext.sail | 26 +-- model/riscv_insts_end.sail | 4 +- model/riscv_insts_fext.sail | 42 ++--- model/riscv_insts_mext.sail | 1 - model/riscv_insts_svinval.sail | 8 +- model/riscv_insts_vext_arith.sail | 247 ++++++++++++++++++++--------- model/riscv_insts_vext_fp.sail | 141 ++++++++++------ model/riscv_insts_vext_fp_red.sail | 18 ++- model/riscv_insts_vext_fp_vm.sail | 14 +- model/riscv_insts_vext_mask.sail | 56 +++++-- model/riscv_insts_vext_mem.sail | 228 +++++++++++++++----------- model/riscv_insts_vext_red.sail | 14 +- model/riscv_insts_vext_utils.sail | 43 +++-- model/riscv_insts_vext_vm.sail | 84 +++++++--- model/riscv_insts_zfa.sail | 12 +- model/riscv_insts_zfh.sail | 30 ++-- model/riscv_insts_zicbom.sail | 13 +- model/riscv_insts_zicboz.sail | 11 +- model/riscv_insts_zicsr.sail | 4 +- model/riscv_jalr_seq.sail | 9 +- model/riscv_platform.sail | 2 +- model/riscv_regs.sail | 3 - model/riscv_step.sail | 78 ++++++--- model/riscv_types.sail | 10 +- 30 files changed, 778 insertions(+), 450 deletions(-) create mode 100644 model/riscv_inst_retire.sail diff --git a/Makefile.old b/Makefile.old index 270ebae31..2221fe925 100644 --- a/Makefile.old +++ b/Makefile.old @@ -107,8 +107,9 @@ SAIL_ARCH_SRCS += riscv_extensions.sail riscv_types_common.sail riscv_types_ext. SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail SAIL_ARCH_SRCS += riscv_sstc.sail SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS) -SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_extensions.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail +SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_extensions.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail riscv_inst_retire.sail SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptography extension. +SAIL_ARCH_SRCS += riscv_inst_retire.sail SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt index bdb598d86..360534bca 100644 --- a/model/CMakeLists.txt +++ b/model/CMakeLists.txt @@ -166,6 +166,7 @@ foreach (xlen IN ITEMS 32 64) ${sail_vm_srcs} # Shared/common code for the cryptography extension. "riscv_types_kext.sail" + "riscv_inst_retire.sail" ) if (variant STREQUAL "rvfi") diff --git a/model/riscv_inst_retire.sail b/model/riscv_inst_retire.sail new file mode 100644 index 000000000..78916fc65 --- /dev/null +++ b/model/riscv_inst_retire.sail @@ -0,0 +1,28 @@ +/*=======================================================================================*/ +/* 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 */ +/*=======================================================================================*/ + +/* Reasons an instruction retire might fail or be incomplete. */ + +union Retire_Failure = { + // standard reasons + Illegal_Instruction : unit, + Wait_For_Interrupt : unit, + Trap : (Privilege, ctl_result, xlenbits), + Memory_Exception : (virtaddr, ExceptionType), + + // reasons from external extensions + Ext_CSR_Check_Failure : unit, + Ext_ControlAddr_Check_Failure : ext_control_addr_error, + Ext_DataAddr_Check_Failure : ext_data_addr_error, + Ext_XRET_Priv_Failure : unit, +} + +// For backwards compatibility, this global definition is used +// instead of the previous RETIRE_SUCCESS enum value. + +let RETIRE_SUCCESS : Retired(Retire_Failure) = RETIRE_OK() diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 8b9963c2e..6ceb886b6 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -80,19 +80,19 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { * Extensions might perform additional checks on address validity. */ match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { /* "LR faults like a normal load, even though it's in the AMO major opcode space." * - Andrew Waterman, isa-dev, 10 Jul 2018. */ if not(is_aligned(virtaddr_bits(vaddr), width)) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(addr, _) => match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) { Ok(result) => { load_reservation(physaddr_bits(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS }, - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), }, } } @@ -128,14 +128,14 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { * Extensions might perform additional checks on address validity. */ match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { if not(is_aligned(virtaddr_bits(vaddr), width)) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else { match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here: * both result in a SAMO exception */ - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(addr, _) => { // Check reservation with physical address. if not(match_reservation(physaddr_bits(addr))) then { @@ -144,13 +144,13 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { } else { let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); match eares { - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let rs2_val = X(rs2); match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) { Ok(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, Ok(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), } } } @@ -198,20 +198,20 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { * Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { if not(is_aligned(virtaddr_bits(vaddr), width)) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, ReadWrite(Data, Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(addr, _) => { let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0]; match eares { - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) { - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(loaded) => { let result : bits('width_bytes * 8) = match op { @@ -228,7 +228,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) { Ok(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS }, Ok(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), } } } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index deed59b98..4057eb834 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -62,16 +62,12 @@ function clause execute (RISCV_JAL(imm, rd)) = { let target = PC + sign_extend(imm); /* Extensions get the first checks on the prospective target address. */ match ext_control_check_pc(target) { - Ext_ControlAddr_Error(e) => { - ext_handle_control_check_error(e); - RETIRE_FAIL - }, + Ext_ControlAddr_Error(e) => RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), Ext_ControlAddr_OK(target) => { /* Perform standard alignment check */ let target_bits = virtaddr_bits(target); if bit_to_bool(target_bits[1]) & not(extensionEnabled(Ext_Zca)) then { - handle_mem_exception(target, E_Fetch_Addr_Align()); - RETIRE_FAIL + RETIRE_FAIL(Memory_Exception(target, E_Fetch_Addr_Align())) } else { X(rd) = get_next_pc(); set_next_pc(target_bits); @@ -125,15 +121,11 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = { let target = PC + sign_extend(imm); /* Extensions get the first checks on the prospective target address. */ match ext_control_check_pc(target) { - Ext_ControlAddr_Error(e) => { - ext_handle_control_check_error(e); - RETIRE_FAIL - }, + Ext_ControlAddr_Error(e) => RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), Ext_ControlAddr_OK(target) => { let target_bits = virtaddr_bits(target); if bit_to_bool(target_bits[1]) & not(extensionEnabled(Ext_Zca)) then { - handle_mem_exception(target, E_Fetch_Addr_Align()); - RETIRE_FAIL + RETIRE_FAIL(Memory_Exception(target, E_Fetch_Addr_Align())) } else { set_next_pc(target_bits); RETIRE_SUCCESS @@ -306,17 +298,16 @@ function clause execute (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => - match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) { Ok(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS }, - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), }, } }, @@ -362,22 +353,22 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares = mem_write_ea(paddr, width_bytes, aq, rl, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let rs2_val = X(rs2); match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) { Ok(true) => RETIRE_SUCCESS, Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -598,8 +589,7 @@ function clause execute ECALL() = { }, excinfo = (None() : option(xlenbits)), ext = None() }; - set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC)); - RETIRE_FAIL + RETIRE_FAIL(Trap(cur_privilege, CTL_TRAP(t), PC)) } mapping clause assembly = ECALL() <-> "ecall" @@ -612,9 +602,9 @@ mapping clause encdec = MRET() function clause execute MRET() = { if cur_privilege != Machine - then { handle_illegal(); RETIRE_FAIL } - else if not(ext_check_xret_priv (Machine)) - then { ext_fail_xret_priv(); RETIRE_FAIL } + then RETIRE_FAIL(Illegal_Instruction()) + else if not(ext_check_xret_priv(Machine)) + then RETIRE_FAIL(Ext_XRET_Priv_Failure()) else { set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC)); RETIRE_SUCCESS @@ -636,9 +626,9 @@ function clause execute SRET() = { Machine => not(extensionEnabled(Ext_S)) }; if sret_illegal - then { handle_illegal(); RETIRE_FAIL } + then RETIRE_FAIL(Illegal_Instruction()) else if not(ext_check_xret_priv (Supervisor)) - then { ext_fail_xret_priv(); RETIRE_FAIL } + then RETIRE_FAIL(Ext_XRET_Priv_Failure()) else { set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)); RETIRE_SUCCESS @@ -653,10 +643,8 @@ union clause ast = EBREAK : unit mapping clause encdec = EBREAK() <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 -function clause execute EBREAK() = { - handle_mem_exception(virtaddr(PC), E_Breakpoint()); - RETIRE_FAIL -} +function clause execute EBREAK() = + RETIRE_FAIL(Memory_Exception(virtaddr(PC), E_Breakpoint())) mapping clause assembly = EBREAK() <-> "ebreak" @@ -668,11 +656,11 @@ mapping clause encdec = WFI() function clause execute WFI() = match cur_privilege { - Machine => { platform_wfi(); RETIRE_SUCCESS }, + Machine => RETIRE_FAIL(Wait_For_Interrupt()), Supervisor => if mstatus[TW] == 0b1 - then { handle_illegal(); RETIRE_FAIL } - else { platform_wfi(); RETIRE_SUCCESS }, - User => { handle_illegal(); RETIRE_FAIL } + then RETIRE_FAIL(Illegal_Instruction()) + else RETIRE_FAIL(Wait_For_Interrupt()), + User => RETIRE_FAIL(Illegal_Instruction()) } mapping clause assembly = WFI() <-> "wfi" @@ -690,9 +678,9 @@ function clause execute SFENCE_VMA(rs1, rs2) = { // is 9 but we always set it to 16 for RV64. let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None(); match cur_privilege { - User => { handle_illegal(); RETIRE_FAIL }, + User => RETIRE_FAIL(Illegal_Instruction()), Supervisor => match mstatus[TVM] { - 0b1 => { handle_illegal(); RETIRE_FAIL }, + 0b1 => RETIRE_FAIL(Illegal_Instruction()), 0b0 => { flush_TLB(asid, addr); RETIRE_SUCCESS }, }, Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS } diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail index 4287535c0..22e28e0fc 100644 --- a/model/riscv_insts_begin.sail +++ b/model/riscv_insts_begin.sail @@ -14,7 +14,7 @@ scattered union ast /* returns whether an instruction was retired, used for computing minstret */ -val execute : ast -> Retired +val execute : ast -> Retired(Retire_Failure) scattered function execute val assembly : ast <-> string diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 40a16e148..4c286c86b 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -279,7 +279,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { let rs3_val_64b = F_or_X_D(rs3); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_64b) : (bits(5), bits(64)) = @@ -344,7 +344,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = { let rs1_val_64b = F_or_X_D(rs1); let rs2_val_64b = F_or_X_D(rs2); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_64b) : (bits(5), bits(64)) = match op { @@ -436,7 +436,7 @@ mapping clause encdec = function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_f64Sqrt (rm_3b, rs1_val_D); @@ -451,7 +451,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_W) = riscv_f64ToI32 (rm_3b, rs1_val_D); @@ -466,7 +466,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = { let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_WU) = riscv_f64ToUi32 (rm_3b, rs1_val_D); @@ -481,7 +481,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = { let rs1_val_W = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W); @@ -496,7 +496,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = { let rs1_val_WU = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU); @@ -511,7 +511,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D); @@ -526,7 +526,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S); @@ -542,7 +542,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { assert(xlen >= 64); let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_L) = riscv_f64ToI64 (rm_3b, rs1_val_D); @@ -558,7 +558,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { assert(xlen >= 64); let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D); @@ -574,7 +574,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = { assert(xlen >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L); @@ -590,7 +590,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = { assert(xlen >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU); diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail index 728c21e43..523982c89 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -12,7 +12,7 @@ mapping clause encdec = ILLEGAL(s) <-> s -function clause execute (ILLEGAL(s)) = { handle_illegal(); RETIRE_FAIL } +function clause execute (ILLEGAL(s)) = RETIRE_FAIL(Illegal_Instruction()) mapping clause assembly = ILLEGAL(s) <-> "illegal" ^ spc() ^ hex_bits_32(s) @@ -20,7 +20,7 @@ mapping clause assembly = ILLEGAL(s) <-> "illegal" ^ spc() ^ hex_bits_32(s) mapping clause encdec_compressed = C_ILLEGAL(s) <-> s -function clause execute C_ILLEGAL(s) = { handle_illegal(); RETIRE_FAIL } +function clause execute C_ILLEGAL(s) = RETIRE_FAIL(Illegal_Instruction()) mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s) diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 4e33c3692..a0176449e 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -298,17 +298,17 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(addr, _) => { let (aq, rl, res) = (false, false, false); match mem_read(Read(Data), addr, width_bytes, aq, rl, res) { Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), } }, } @@ -356,21 +356,21 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(addr, _) => { match mem_write_ea(addr, width_bytes, aq, rl, false) { - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let rs2_val = F(rs2); match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, con) { - Ok(true) => { RETIRE_SUCCESS }, + Ok(true) => RETIRE_SUCCESS, Ok(false) => { internal_error(__FILE__, __LINE__, "store got false from mem_write_value") }, - Err(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)) } }, } @@ -420,7 +420,7 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = { let rs2_val_32b = F_or_X_S(rs2); let rs3_val_32b = F_or_X_S(rs3); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_32b) : (bits(5), bits(32)) = @@ -485,7 +485,7 @@ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = { let rs1_val_32b = F_or_X_S(rs1); let rs2_val_32b = F_or_X_S(rs2); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_32b) : (bits(5), bits(32)) = match op { @@ -569,7 +569,7 @@ mapping clause encdec = function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_f32Sqrt (rm_3b, rs1_val_S); @@ -584,7 +584,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = { function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_W) = riscv_f32ToI32 (rm_3b, rs1_val_S); @@ -599,7 +599,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_WU) = riscv_f32ToUi32 (rm_3b, rs1_val_S); @@ -614,7 +614,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = { function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = { let rs1_val_W = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W); @@ -629,7 +629,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = { function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = { let rs1_val_WU = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU); @@ -645,7 +645,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = { assert(xlen >= 64); let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_L) = riscv_f32ToI64 (rm_3b, rs1_val_S); @@ -661,7 +661,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = { assert(xlen >= 64); let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_LU) = riscv_f32ToUi64 (rm_3b, rs1_val_S); @@ -677,7 +677,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = { assert(xlen >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L); @@ -693,7 +693,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = { assert(xlen >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU); diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index 20a928119..95b6a5ef7 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -14,7 +14,6 @@ function clause extensionEnabled(Ext_M) = misa[M] == 0b1 function clause extensionEnabled(Ext_Zmmul) = true - union clause ast = MUL : (regidx, regidx, regidx, mul_op) mapping encdec_mul_op : mul_op <-> bits(3) = { diff --git a/model/riscv_insts_svinval.sail b/model/riscv_insts_svinval.sail index 34c2a753f..80880d741 100644 --- a/model/riscv_insts_svinval.sail +++ b/model/riscv_insts_svinval.sail @@ -31,8 +31,8 @@ mapping clause encdec = function clause execute SFENCE_W_INVAL() = { if cur_privilege == User - then { handle_illegal(); RETIRE_FAIL } - else { RETIRE_SUCCESS } // Implemented as no-op as all memory operations are visible immediately the current Sail model + then RETIRE_FAIL(Illegal_Instruction()) + else RETIRE_SUCCESS // Implemented as no-op as all memory operations are visible immediately the current Sail model } mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval" @@ -47,8 +47,8 @@ mapping clause encdec = function clause execute SFENCE_INVAL_IR() = { if cur_privilege == User - then { handle_illegal(); RETIRE_FAIL } - else { RETIRE_SUCCESS } // Implemented as no-op as all memory operations are visible immediately in current Sail model + then RETIRE_FAIL(Illegal_Instruction()) + else RETIRE_SUCCESS // Implemented as no-op as all memory operations are visible immediately in current Sail model } mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir" diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 915367248..b8d9dde12 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -50,7 +50,7 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { let VLEN_pow = get_vlen_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -60,7 +60,10 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -113,14 +116,14 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { VV_VMAXU => to_bits(SEW, max(unsigned(vs2_val[i]), unsigned(vs1_val[i]))), VV_VMAX => to_bits(SEW, max(signed(vs2_val[i]), signed(vs1_val[i]))), VV_VRGATHER => { - if (vs1 == vd | vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs1 == vd | vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); let idx = unsigned(vs1_val[i]); let VLMAX = 2 ^ (LMUL_pow + VLEN_pow - SEW_pow); assert(VLMAX <= 'n); if idx < VLMAX then vs2_val[idx] else zeros() }, VV_VRGATHEREI16 => { - if (vs1 == vd | vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs1 == vd | vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); /* vrgatherei16.vv uses SEW/LMUL for the data in vs2 but EEW=16 and EMUL = (16/SEW)*LMUL for the indices in vs1 */ let vs1_new : vector('n, bits(16)) = read_vreg(num_elem, 16, 4 + LMUL_pow - SEW_pow, vs1); let idx = unsigned(vs1_new[i]); @@ -185,7 +188,7 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -196,7 +199,10 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW_widen <= 64); @@ -251,7 +257,7 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -262,7 +268,10 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW_widen <= 64); @@ -304,14 +313,17 @@ mapping clause encdec = MASKTYPEV (vs2, vs1, vd) if extensionEnabled(Ext_V) <-> 0b010111 @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MASKTYPEV(vs2, vs1, vd)) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let end_element = get_end_element(); let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -356,7 +368,7 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -365,7 +377,10 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -414,7 +429,7 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -424,7 +439,10 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -533,7 +551,7 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -544,7 +562,10 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW_widen <= 64); @@ -599,7 +620,7 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -610,7 +631,10 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW_widen <= 64); @@ -665,7 +689,7 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let VLEN_pow = get_vlen_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -675,14 +699,17 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] == bitone then { result[i] = match funct6 { VX_VSLIDEUP => { - if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); if i >= rs1_val then vs2_val[i - rs1_val] else vd_val[i] }, VX_VSLIDEDOWN => { @@ -691,7 +718,7 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { if i + rs1_val < VLMAX then vs2_val[i + rs1_val] else zeros() }, VX_VRGATHER => { - if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); let VLMAX = 2 ^ (LMUL_pow + VLEN_pow - SEW_pow); assert(VLMAX > 0 & VLMAX <= 'n); if rs1_val < VLMAX then vs2_val[rs1_val] else zeros() @@ -721,14 +748,17 @@ mapping clause encdec = MASKTYPEX(vs2, rs1, vd) if extensionEnabled(Ext_V) <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MASKTYPEX(vs2, rs1, vd)) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let end_element = get_end_element(); let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -773,7 +803,7 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -782,7 +812,10 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -823,7 +856,7 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -833,7 +866,10 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -918,7 +954,7 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -929,7 +965,10 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW_widen <= 64); @@ -984,7 +1023,7 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -995,7 +1034,10 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW_widen <= 64); @@ -1050,7 +1092,7 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let VLEN_pow = get_vlen_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1060,14 +1102,17 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] == bitone then { result[i] = match funct6 { VI_VSLIDEUP => { - if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); if i >= imm_val then vs2_val[i - imm_val] else vd_val[i] }, VI_VSLIDEDOWN => { @@ -1076,7 +1121,7 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { if i + imm_val < VLMAX then vs2_val[i + imm_val] else zeros() }, VI_VRGATHER => { - if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); let VLMAX = 2 ^ (LMUL_pow + VLEN_pow - SEW_pow); assert(VLMAX > 0 & VLMAX <= 'n); if imm_val < VLMAX then vs2_val[imm_val] else zeros() @@ -1106,14 +1151,17 @@ mapping clause encdec = MASKTYPEI(vs2, simm, vd) if extensionEnabled(Ext_V) <-> 0b010111 @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MASKTYPEI(vs2, simm, vd)) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let end_element = get_end_element(); let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1158,7 +1206,7 @@ function clause execute(MOVETYPEI(vd, simm)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1167,7 +1215,10 @@ function clause execute(MOVETYPEI(vd, simm)) = { let imm_val : bits('m) = sign_extend(simm); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1189,12 +1240,15 @@ mapping clause encdec = VMVRTYPE(vs2, simm, vd) if extensionEnabled(Ext_V) <-> 0b100111 @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMVRTYPE(vs2, simm, vd)) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let SEW = get_sew(); let imm_val = unsigned(zero_extend(xlen, simm)); let EMUL = imm_val + 1; - if not(EMUL == 1 | EMUL == 2 | EMUL == 4 | EMUL == 8) then { handle_illegal(); return RETIRE_FAIL }; + if not(EMUL == 1 | EMUL == 2 | EMUL == 4 | EMUL == 8) then return RETIRE_FAIL(Illegal_Instruction()); let EMUL_pow = log2(EMUL); let num_elem = get_num_elem(EMUL_pow, SEW); @@ -1251,7 +1305,7 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1261,7 +1315,10 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1359,7 +1416,7 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1369,7 +1426,10 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1423,7 +1483,7 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1434,7 +1494,10 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1491,7 +1554,7 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1502,7 +1565,10 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1554,7 +1620,7 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1565,7 +1631,10 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1613,7 +1682,7 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { if illegal_variable_width(vd, vm, SEW_half, LMUL_pow_half) | not(valid_reg_overlap(vs2, vd, LMUL_pow_half, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1623,7 +1692,10 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1669,7 +1741,7 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { if illegal_variable_width(vd, vm, SEW_quart, LMUL_pow_quart) | not(valid_reg_overlap(vs2, vd, LMUL_pow_quart, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1679,7 +1751,10 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1725,7 +1800,7 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { if illegal_variable_width(vd, vm, SEW_eighth, LMUL_pow_eighth) | not(valid_reg_overlap(vs2, vd, LMUL_pow_eighth, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1735,7 +1810,10 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; assert(SEW > SEW_eighth); @@ -1771,7 +1849,7 @@ function clause execute(VMVXS(vs2, rd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); assert(num_elem > 0); let 'n = num_elem; @@ -1796,7 +1874,10 @@ mapping clause encdec = MVVCOMPRESS(vs2, vs1, vd) if extensionEnabled(Ext_V) <-> 0b010111 @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let end_element = get_end_element(); let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); @@ -1804,7 +1885,7 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { /* vcompress should always be executed with a vstart of 0 */ if start_element != 0 | vs1 == vd | vs2 == vd | illegal_vd_unmasked() - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1874,7 +1955,7 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -1884,7 +1965,10 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1911,7 +1995,7 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { slice(result_sub >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVX_VSLIDE1UP => { - if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; + if (vs2 == vd) then return RETIRE_FAIL(Illegal_Instruction()); if i == 0 then rs1_val else vs2_val[i - 1] }, MVX_VSLIDE1DOWN => { @@ -1993,7 +2077,7 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -2003,7 +2087,10 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -2057,7 +2144,7 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -2068,7 +2155,10 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -2124,7 +2214,7 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow_widen = LMUL_pow + 1; if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -2135,7 +2225,10 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -2187,7 +2280,7 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -2198,7 +2291,10 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -2237,7 +2333,7 @@ function clause execute(VMVSX(rs1, vd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); assert(num_elem > 0); let 'n = num_elem; @@ -2247,7 +2343,10 @@ function clause execute(VMVSX(rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, 'm); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, 0, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; /* one body element */ diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index c39869ef7..658641f90 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -36,7 +36,7 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -47,7 +47,10 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -110,7 +113,7 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -121,7 +124,10 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -181,7 +187,7 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; @@ -193,7 +199,10 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -245,7 +254,7 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; @@ -257,7 +266,10 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -307,7 +319,7 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; @@ -319,7 +331,10 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -365,7 +380,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -375,7 +390,10 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -482,7 +500,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 8 & SEW_widen <= 64); let 'n = num_elem; @@ -493,7 +511,10 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -501,7 +522,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { result[i] = match vfwunary0 { FWV_CVT_XU_F => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f16ToUi32(rm_3b, vs2_val[i]), 32 => riscv_f32ToUi64(rm_3b, vs2_val[i]) }; @@ -510,7 +531,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { }, FWV_CVT_X_F => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f16ToI32(rm_3b, vs2_val[i]), 32 => riscv_f32ToI64(rm_3b, vs2_val[i]) }; @@ -537,7 +558,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { }, FWV_CVT_F_F => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f16ToF32(rm_3b, vs2_val[i]), 32 => riscv_f32ToF64(rm_3b, vs2_val[i]) }; @@ -546,7 +567,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { }, FWV_CVT_RTZ_XU_F => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f16ToUi32(0b001, vs2_val[i]), 32 => riscv_f32ToUi64(0b001, vs2_val[i]) }; @@ -555,7 +576,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { }, FWV_CVT_RTZ_X_F => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f16ToI32(0b001, vs2_val[i]), 32 => riscv_f32ToI64(0b001, vs2_val[i]) }; @@ -611,7 +632,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 64); let 'n = num_elem; @@ -622,7 +643,10 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -648,7 +672,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { }, FNV_CVT_F_XU => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_ui32ToF16(rm_3b, vs2_val[i]), 32 => riscv_ui64ToF32(rm_3b, vs2_val[i]) }; @@ -657,7 +681,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { }, FNV_CVT_F_X => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_i32ToF16(rm_3b, vs2_val[i]), 32 => riscv_i64ToF32(rm_3b, vs2_val[i]) }; @@ -666,7 +690,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { }, FNV_CVT_F_F => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f32ToF16(rm_3b, vs2_val[i]), 32 => riscv_f64ToF32(rm_3b, vs2_val[i]) }; @@ -675,7 +699,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { }, FNV_CVT_ROD_F_F => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { - 8 => { handle_illegal(); return RETIRE_FAIL }, + 8 => return RETIRE_FAIL(Illegal_Instruction()), 16 => riscv_f32ToF16(0b110, vs2_val[i]), 32 => riscv_f64ToF32(0b110, vs2_val[i]) }; @@ -742,7 +766,7 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -752,7 +776,10 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -817,7 +844,7 @@ function clause execute(VFMVFS(vs2, rd)) = { let num_elem = get_num_elem(0, SEW); if illegal_fp_vd_unmasked(SEW, rm_3b) | SEW > flen - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(num_elem > 0 & SEW != 8); let 'n = num_elem; @@ -865,7 +892,7 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -876,7 +903,10 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -894,7 +924,7 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { VF_VSGNJN => (0b1 ^ [rs1_val['m - 1]]) @ vs2_val[i][('m - 2)..0], VF_VSGNJX => ([vs2_val[i]['m - 1]] ^ [rs1_val['m - 1]]) @ vs2_val[i][('m - 2)..0], VF_VSLIDE1UP => { - if vs2 == vd then { handle_illegal(); return RETIRE_FAIL }; + if vs2 == vd then return RETIRE_FAIL(Illegal_Instruction()); if i == 0 then rs1_val else vs2_val[i - 1] }, VF_VSLIDE1DOWN => { @@ -954,7 +984,7 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -965,7 +995,10 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1024,7 +1057,7 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; @@ -1036,7 +1069,10 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1087,7 +1123,7 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; @@ -1099,7 +1135,10 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1148,7 +1187,7 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow_widen = LMUL_pow + 1; if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; @@ -1160,7 +1199,10 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('o)), bits('n)) = match init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1194,14 +1236,17 @@ mapping clause encdec = VFMERGE(vs2, rs1, vd) if extensionEnabled(Ext_V) function clause execute(VFMERGE(vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let end_element = get_end_element(); let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if illegal_fp_vd_masked(vd, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_masked(vd, SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -1249,7 +1294,7 @@ function clause execute(VFMV(rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -1259,7 +1304,10 @@ function clause execute(VFMV(rs1, vd)) = { let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -1285,7 +1333,7 @@ function clause execute(VFMVSF(rs1, vd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(num_elem > 0 & SEW != 8); let 'n = num_elem; @@ -1295,7 +1343,10 @@ function clause execute(VFMVSF(rs1, vd)) = { let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, 0, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; /* one body element */ diff --git a/model/riscv_insts_vext_fp_red.sail b/model/riscv_insts_vext_fp_red.sail index 8e7ad210f..74996ac09 100755 --- a/model/riscv_insts_vext_fp_red.sail +++ b/model/riscv_insts_vext_fp_red.sail @@ -26,12 +26,12 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = { mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) -val process_rfvv_single: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired +val process_rfvv_single: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired(Retire_Failure) function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr[FRM]; let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ - if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_reduction(SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ @@ -43,7 +43,10 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = match init_masked_source(num_elem_vs, LMUL_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { @@ -66,14 +69,14 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po RETIRE_SUCCESS } -val process_rfvv_widen: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired +val process_rfvv_widen: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired(Retire_Failure) function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr[FRM]; let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ - if illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW >= 16 & SEW_widen <= 64); if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ @@ -86,7 +89,10 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = match init_masked_source(num_elem_vs, LMUL_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail index dafd1d4d3..9bfa7a5be 100755 --- a/model/riscv_insts_vext_fp_vm.sail +++ b/model/riscv_insts_vext_fp_vm.sail @@ -31,7 +31,7 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -42,7 +42,10 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -94,7 +97,7 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then return RETIRE_FAIL(Illegal_Instruction()); assert(SEW != 8); let 'n = num_elem; @@ -105,7 +108,10 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index 72147c20a..48ea56fb5 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -33,7 +33,7 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = VLEN; - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -42,7 +42,10 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, 0, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -90,7 +93,7 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = VLEN; - if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() | not(assert_vstart(0)) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -98,7 +101,10 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); - let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); + let (_, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var count : nat = 0; foreach (i from 0 to (num_elem - 1)) { @@ -124,7 +130,7 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = VLEN; - if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() | not(assert_vstart(0)) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -132,7 +138,10 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); - let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); + let (_, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var index : int = -1; foreach (i from 0 to (num_elem - 1)) { @@ -161,7 +170,7 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = { let num_elem = VLEN; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -170,7 +179,10 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = { let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; var found_elem : bool = false; @@ -201,7 +213,7 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = { let num_elem = VLEN; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -210,7 +222,10 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = { let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; var found_elem : bool = false; @@ -241,7 +256,7 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = { let num_elem = VLEN; if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -250,7 +265,10 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = { let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; var found_elem : bool = false; @@ -285,7 +303,7 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { let num_elem = get_num_elem(LMUL_pow, SEW); if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 - then { handle_illegal(); return RETIRE_FAIL }; + then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -294,7 +312,10 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; var sum : int = 0; @@ -324,7 +345,7 @@ function clause execute(VID_V(vm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -332,7 +353,10 @@ function clause execute(VID_V(vm, vd)) = { let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 8635a8b48..01236546b 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -67,14 +67,19 @@ union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired +val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired(Retire_Failure) function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : bits('n) = 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 (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); + let 'n = num_elem; + let 'm = nf * load_width_bytes * 8; + let (result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; foreach (i from 0 to (num_elem - 1)) { if mask[i] == bitone then { /* active segments */ @@ -82,16 +87,16 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { Ok(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -121,7 +126,7 @@ function clause execute(VLSEGTYPE(nf, vm, rs1, width, vd)) = { assert(num_elem > 0); - if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then return RETIRE_FAIL(Illegal_Instruction()); process_vlseg(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -135,7 +140,7 @@ union clause ast = VLSEGFFTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired +val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired(Retire_Failure) function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); @@ -143,7 +148,12 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let tail_ag : agtype = get_vtype_vta(); - let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); + let 'n = num_elem; + let 'm = nf * load_width_bytes * 8; + let (result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var trimmed : bool = false; foreach (i from 0 to (num_elem - 1)) { @@ -153,7 +163,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) let elem_offset = (i * nf + j) * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { - if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } + if i == 0 then return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)) else { vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); @@ -162,7 +172,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) }, Ext_DataAddr_OK(vaddr) => { if check_misaligned(vaddr, width_type) then { - if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + if i == 0 then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else { vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); @@ -170,7 +180,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { - if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + if i == 0 then return RETIRE_FAIL(Memory_Exception(vaddr, e)) else { vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); @@ -181,7 +191,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { Ok(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), Err(e) => { - if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + if i == 0 then return RETIRE_FAIL(Memory_Exception(vaddr, e)) else { vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); @@ -228,7 +238,7 @@ function clause execute(VLSEGFFTYPE(nf, vm, rs1, width, vd)) = { assert(num_elem > 0); - if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then return RETIRE_FAIL(Illegal_Instruction()); process_vlsegff(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -242,13 +252,18 @@ union clause ast = VSSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired +val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired(Retire_Failure) function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : bits('n) = 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 mask : bits('n) = init_masked_source(num_elem, EMUL_pow, vm_val); + + let 'n = num_elem; + let mask : bits('n) = match init_masked_source(num_elem, EMUL_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; foreach (i from 0 to (num_elem - 1)) { if mask[i] == bitone then { /* active segments */ @@ -256,23 +271,23 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg)); let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); match (res) { Ok(true) => (), Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -299,7 +314,7 @@ function clause execute(VSSEGTYPE(nf, vm, rs1, width, vs3)) = { assert(num_elem > 0); - if illegal_store(nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_store(nf_int, EEW, EMUL_pow) then return RETIRE_FAIL(Illegal_Instruction()); process_vsseg(nf_int, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -313,7 +328,7 @@ union clause ast = VLSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired +val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired(Retire_Failure) function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); @@ -321,7 +336,12 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e 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 = unsigned(get_scalar(rs2, xlen)); - let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); + let 'n = num_elem; + let 'm = nf * load_width_bytes * 8; + let (result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; foreach (i from 0 to (num_elem - 1)) { if mask[i] == bitone then { /* active segments */ @@ -329,16 +349,16 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { Ok(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -368,7 +388,7 @@ function clause execute(VLSSEGTYPE(nf, vm, rs2, rs1, width, vd)) = { assert(num_elem > 0); - if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then return RETIRE_FAIL(Illegal_Instruction()); process_vlsseg(nf_int, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -382,14 +402,19 @@ union clause ast = VSSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired +val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired(Retire_Failure) function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); let vm_val : bits('n) = 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 = unsigned(get_scalar(rs2, xlen)); - let mask : bits('n) = init_masked_source(num_elem, EMUL_pow, vm_val); + + let 'n = num_elem; + let mask : bits('n) = match init_masked_source(num_elem, EMUL_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; foreach (i from 0 to (num_elem - 1)) { if mask[i] == bitone then { /* active segments */ @@ -397,23 +422,23 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg)); let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false); match (res) { Ok(true) => (), Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -440,7 +465,7 @@ function clause execute(VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3)) = { assert(num_elem > 0); - if illegal_store(nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_store(nf_int, EEW, EMUL_pow) then return RETIRE_FAIL(Illegal_Instruction()); process_vssseg(nf_int, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -454,7 +479,7 @@ union clause ast = VLUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired +val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired(Retire_Failure) function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow; let width_type : word_width = size_bytes(EEW_data_bytes); @@ -462,7 +487,12 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index let vd_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); - let (result, mask) = init_masked_result(num_elem, nf * EEW_data_bytes * 8, EMUL_data_pow, vd_seg, vm_val); + let 'n = num_elem; + let 'm = nf * EEW_data_bytes * 8; + let (result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, nf * EEW_data_bytes * 8, EMUL_data_pow, vd_seg, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { @@ -471,16 +501,16 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index foreach (j from 0 to (nf - 1)) { 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_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { Ok(elem) => write_single_element(EEW_data_bytes * 8, i, vd + to_bits(5, j * EMUL_data_reg), elem), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -510,7 +540,8 @@ function clause execute(VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { assert(num_elem > 0); - if illegal_indexed_load(vd, vm, nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_indexed_load(vd, vm, nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) + then return RETIRE_FAIL(Illegal_Instruction()); process_vlxseg(nf_int, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) } @@ -536,7 +567,8 @@ function clause execute(VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { assert(num_elem > 0); - if illegal_indexed_load(vd, vm, nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_indexed_load(vd, vm, nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) + then return RETIRE_FAIL(Illegal_Instruction()); process_vlxseg(nf_int, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) } @@ -550,14 +582,19 @@ union clause ast = VSUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired +val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired(Retire_Failure) function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow; let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); - let mask : bits('n) = init_masked_source(num_elem, EMUL_data_pow, vm_val); + + let 'n = num_elem; + let mask : bits('n) = match init_masked_source(num_elem, EMUL_data_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { @@ -566,23 +603,23 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde foreach (j from 0 to (nf - 1)) { 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_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let elem_val : bits('db * 8) = read_single_element(EEW_data_bytes * 8, i, vs3 + to_bits(5, j * EMUL_data_reg)); let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, elem_val, false, false, false); match (res) { Ok(true) => (), Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -609,7 +646,8 @@ function clause execute(VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { assert(num_elem > 0); - if illegal_indexed_store(nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_indexed_store(nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) + then return RETIRE_FAIL(Illegal_Instruction()); process_vsxseg(nf_int, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) } @@ -635,7 +673,8 @@ function clause execute(VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { assert(num_elem > 0); - if illegal_indexed_store(nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_indexed_store(nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) + then return RETIRE_FAIL(Illegal_Instruction()); process_vsxseg(nf_int, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) } @@ -649,10 +688,13 @@ union clause ast = VLRETYPE : (bits(3), regidx, vlewidth, regidx) mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired +val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired(Retire_Failure) function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { let width_type : word_width = size_bytes(load_width_bytes); - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ let elem_to_align : int = start_element % elem_per_reg; var cur_field : int = start_element / elem_per_reg; @@ -663,16 +705,16 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { set_vstart(to_bits(16, cur_elem)); let elem_offset = cur_elem * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { Ok(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, cur_field), elem), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -687,16 +729,16 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { set_vstart(to_bits(16, cur_elem)); let elem_offset = cur_elem * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { Ok(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j), elem), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -716,7 +758,7 @@ function clause execute(VLRETYPE(nf, rs1, width, vd)) = { let nf_int = nfields_int(nf); assert(elem_per_reg >= 0); - if not(nf_int == 1 | nf_int == 2 | nf_int == 4 | nf_int == 8) then { handle_illegal(); return RETIRE_FAIL }; + if not(nf_int == 1 | nf_int == 2 | nf_int == 4 | nf_int == 8) then return RETIRE_FAIL(Illegal_Instruction()); process_vlre(nf_int, vd, load_width_bytes, rs1, elem_per_reg) } @@ -730,10 +772,13 @@ union clause ast = VSRETYPE : (bits(3), regidx, regidx) mapping clause encdec = VSRETYPE(nf, rs1, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired +val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired(Retire_Failure) function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { let width_type : word_width = BYTE; - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */ let elem_to_align : int = start_element % elem_per_reg; var cur_field : int = start_element / elem_per_reg; @@ -744,23 +789,23 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { set_vstart(to_bits(16, cur_elem)); let elem_offset : int = cur_elem * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let elem : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, cur_field)); let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem, false, false, false); match (res) { Ok(true) => (), Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -778,22 +823,22 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { set_vstart(to_bits(16, cur_elem)); let elem_offset = cur_elem * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false); match (res) { Ok(true) => (), Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -815,7 +860,7 @@ function clause execute(VSRETYPE(nf, rs1, vs3)) = { let nf_int = nfields_int(nf); assert(elem_per_reg >= 0); - if not(nf_int == 1 | nf_int == 2 | nf_int == 4 | nf_int == 8) then { handle_illegal(); return RETIRE_FAIL }; + if not(nf_int == 1 | nf_int == 2 | nf_int == 4 | nf_int == 8) then return RETIRE_FAIL(Illegal_Instruction()); process_vsre(nf_int, load_width_bytes, rs1, vs3, elem_per_reg) } @@ -834,10 +879,13 @@ mapping encdec_lsop : vmlsop <-> bits(7) = { mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V) <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if extensionEnabled(Ext_V) -val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired +val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired(Retire_Failure) function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { let width_type : word_width = BYTE; - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; let vd_or_vs3_val : vector('n, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3); foreach (i from start_element to (num_elem - 1)) { @@ -845,38 +893,38 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { set_vstart(to_bits(16, i)); if op == VLM then { /* load */ match ext_data_get_addr(rs1, to_bits(xlen, i), Read(Data), 1) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align())) else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, 1, false, false, false) { Ok(elem) => write_single_element(8, i, vd_or_vs3, elem), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } } } else if op == VSM then { /* store */ match ext_data_get_addr(rs1, to_bits(xlen, i), Write(Data), 1) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, + Ext_DataAddr_Error(e) => return RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } + then return RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align())) else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + TR_Failure(e, _) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); match (eares) { - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)), Ok(_) => { let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, vd_or_vs3_val[i], false, false, false); match (res) { Ok(true) => (), Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } + Err(e) => return RETIRE_FAIL(Memory_Exception(vaddr, e)) } } } @@ -903,7 +951,7 @@ function clause execute(VMTYPE(rs1, vd_or_vs3, op)) = { let evl : int = if vl_val % 8 == 0 then vl_val / 8 else vl_val / 8 + 1; /* the effective vector length is evl=ceil(vl/8) */ let num_elem = get_num_elem(EMUL_pow, EEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); assert(evl >= 0); process_vm(vd_or_vs3, rs1, num_elem, evl, op) diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 5b8296587..04fba0ec9 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -30,7 +30,7 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let num_elem_vs = get_num_elem(LMUL_pow, SEW); let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ - if illegal_reduction_widen(SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_reduction_widen(SEW_widen, LMUL_pow_widen) then return RETIRE_FAIL(Illegal_Instruction()); if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ @@ -42,7 +42,10 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = match init_masked_source(num_elem_vs, LMUL_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { @@ -93,7 +96,7 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let num_elem_vs = get_num_elem(LMUL_pow, SEW); let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ - if illegal_reduction() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_reduction() then return RETIRE_FAIL(Illegal_Instruction()); if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ @@ -104,7 +107,10 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = match init_masked_source(num_elem_vs, LMUL_pow, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 6ada9e373..39a0a2ec9 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -173,7 +173,7 @@ function get_scalar(rs1, SEW) = { } /* Get the starting element index from csr vtype */ -val get_start_element : unit -> nat +val get_start_element : unit -> result(nat, unit) function get_start_element() = { let start_element = unsigned(vstart); let VLEN_pow = get_vlen_pow(); @@ -183,8 +183,9 @@ function get_start_element() = { It is recommended that implementations trap if vstart is out of bounds. It is not required to trap, as a possible future use of upper vstart bits is to store imprecise trap information. */ - if start_element > (2 ^ (3 + VLEN_pow - SEW_pow) - 1) then handle_illegal(); - start_element + if start_element > (2 ^ (3 + VLEN_pow - SEW_pow) - 1) + then Err(()) + else Ok(start_element) } /* Get the ending element index from csr vl */ @@ -199,9 +200,12 @@ function get_end_element() = unsigned(vl) - 1 * vector2 is a "mask" vector that is true for an element if the corresponding element * in the result vector should be updated by the calling instruction */ -val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vector('n, bits('m)), bits('n)) -> (vector('n, bits('m)), bits('n)) +val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vector('n, bits('m)), bits('n)) -> result((vector('n, bits('m)), bits('n)), unit) function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return Err(()) + }; let end_element = get_end_element(); let tail_ag : agtype = get_vtype_vta(); let mask_ag : agtype = get_vtype_vma(); @@ -244,7 +248,7 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { } }; - (result, mask) + Ok((result, mask)) } /* For instructions like vector reduction and vector store, @@ -252,9 +256,12 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { * (vs3 for store and vs2 for reduction). There's no destination register to be masked. * In these cases, this function can be called to simply get the mask vector for vs (without the prepared vd result vector). */ -val init_masked_source : forall 'n 'p, 'n > 0. (int('n), int('p), bits('n)) -> bits('n) +val init_masked_source : forall 'n 'p, 'n > 0. (int('n), int('p), bits('n)) -> result(bits('n), unit) function init_masked_source(num_elem, LMUL_pow, vm_val) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return Err(()) + }; let end_element = get_end_element(); var mask : bits('n) = undefined; @@ -281,14 +288,17 @@ function init_masked_source(num_elem, LMUL_pow, vm_val) = { } }; - mask + Ok(mask) } /* Mask handling for carry functions that use masks as input/output */ /* Only prestart and tail elements are masked in a mask value */ -val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), bits('n)) -> (bits('n), bits('n)) +val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), bits('n)) -> result((bits('n), bits('n)), unit) function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return Err(()) + }; let end_element = get_end_element(); var mask : bits('n) = undefined; var result : bits('n) = undefined; @@ -318,13 +328,16 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { } }; - (result, mask) + Ok(result, mask) } /* Mask handling for cmp functions that use masks as output */ -val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), bits('n), bits('n)) -> (bits('n), bits('n)) +val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), bits('n), bits('n)) -> result((bits('n), bits('n)), unit) function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { - let start_element = get_start_element(); + let start_element : nat = match get_start_element() { + Ok(v) => v, + Err(()) => return Err(()) + }; let end_element = get_end_element(); let mask_ag : agtype = get_vtype_vma(); var mask : bits('n) = undefined; @@ -362,7 +375,7 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { } }; - (result, mask) + Ok(result, mask) } /* For vector load/store segment instructions: diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 801262f96..bb3db422f 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -30,7 +30,7 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -40,7 +40,10 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -85,7 +88,7 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -94,7 +97,10 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -139,7 +145,7 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -152,7 +158,10 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -198,7 +207,7 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -208,7 +217,10 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -261,7 +273,7 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -271,7 +283,10 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -316,7 +331,7 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -325,7 +340,10 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -370,7 +388,7 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -383,7 +401,10 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -431,7 +452,7 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -441,7 +462,10 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -497,7 +521,7 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -507,7 +531,10 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -549,7 +576,7 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -558,7 +585,10 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -600,7 +630,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -613,7 +643,10 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues); + let (initial_result, mask) : (vector('n, bits('m)), bits('n)) = match init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -657,7 +690,7 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then return RETIRE_FAIL(Illegal_Instruction()); let 'n = num_elem; let 'm = SEW; @@ -667,7 +700,10 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); - let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) { + Ok(v) => v, + Err(()) => return RETIRE_FAIL(Illegal_Instruction()) + }; var result = initial_result; foreach (i from 0 to (num_elem - 1)) { diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index e93b6c8c1..51875dc5c 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -351,7 +351,7 @@ function clause execute (RISCV_FROUND_H(rs1, rm, rd)) = { let rs1_val_H = F_H(rs1); match (select_instr_or_fcsr_rm(rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, false); @@ -379,7 +379,7 @@ function clause execute (RISCV_FROUNDNX_H(rs1, rm, rd)) = { let rs1_val_H = F_H(rs1); match (select_instr_or_fcsr_rm(rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, true); @@ -407,7 +407,7 @@ function clause execute (RISCV_FROUND_S(rs1, rm, rd)) = { let rs1_val_S = F_S(rs1); match (select_instr_or_fcsr_rm(rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, false); @@ -435,7 +435,7 @@ function clause execute (RISCV_FROUNDNX_S(rs1, rm, rd)) = { let rs1_val_S = F_S(rs1); match (select_instr_or_fcsr_rm(rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, true); @@ -463,7 +463,7 @@ function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = { let rs1_val_D = F_D(rs1); match (select_instr_or_fcsr_rm(rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, false); @@ -491,7 +491,7 @@ function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = { let rs1_val_D = F_D(rs1); match (select_instr_or_fcsr_rm(rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, true); diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index a8c8aff53..0e96be6e2 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -207,7 +207,7 @@ function clause execute (F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)) = { let rs1_val_16b = F_or_X_H(rs1); let rs2_val_16b = F_or_X_H(rs2); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => return RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_16b) : (bits(5), bits(16)) = match op { @@ -271,7 +271,7 @@ function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = { let rs2_val_16b = F_or_X_H(rs2); let rs3_val_16b = F_or_X_H(rs3); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_16b) : (bits(5), bits(16)) = @@ -581,7 +581,7 @@ mapping clause encdec = function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_f16Sqrt (rm_3b, rs1_val_H); @@ -596,7 +596,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_W) = riscv_f16ToI32 (rm_3b, rs1_val_H); @@ -611,7 +611,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_WU) = riscv_f16ToUi32 (rm_3b, rs1_val_H); @@ -626,7 +626,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)) = { let rs1_val_W = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_i32ToF16 (rm_3b, rs1_val_W); @@ -641,7 +641,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)) = { let rs1_val_WU = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_ui32ToF16 (rm_3b, rs1_val_WU); @@ -656,7 +656,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_f32ToF16 (rm_3b, rs1_val_S); @@ -671,7 +671,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = { let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_f64ToF16 (rm_3b, rs1_val_D); @@ -686,7 +686,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_f16ToF32 (rm_3b, rs1_val_H); @@ -702,7 +702,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_D) = riscv_f16ToF64 (rm_3b, rs1_val_H); @@ -718,7 +718,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = { assert(xlen >= 64); let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_L) = riscv_f16ToI64 (rm_3b, rs1_val_H); @@ -734,7 +734,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)) = { assert(xlen >= 64); let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_LU) = riscv_f16ToUi64 (rm_3b, rs1_val_H); @@ -750,7 +750,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)) = { assert(xlen >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_i64ToF16 (rm_3b, rs1_val_L); @@ -766,7 +766,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)) = { assert(xlen >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { - None() => { handle_illegal(); RETIRE_FAIL }, + None() => RETIRE_FAIL(Illegal_Instruction()), Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_H) = riscv_ui64ToF16 (rm_3b, rs1_val_LU); diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index 53c2da94b..73203e832 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -35,7 +35,7 @@ mapping cbop_mnemonic : cbop_zicbom <-> string = { mapping clause assembly = RISCV_ZICBOM(cbop, rs1) <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" -val process_clean_inval : (regidx, cbop_zicbom) -> Retired +val process_clean_inval : (regidx, cbop_zicbom) -> Retired(Retire_Failure) function process_clean_inval(rs1, cbop) = { let rs1_val = X(rs1); let cache_block_size_exp = plat_cache_block_size_exp(); @@ -49,7 +49,7 @@ function process_clean_inval(rs1, cbop) = { // to be in bounds here, whereas `ext_data_get_addr()` checks that all bytes // are in bounds. We will need to add a new function, parameter or access type. match ext_data_get_addr(rs1, negative_offset, Read(Data), cache_block_size) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { let res : option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { TR_Address(paddr, _) => { @@ -94,8 +94,7 @@ function process_clean_inval(rs1, cbop) = { // was encoded in the instruction. We subtract the negative offset // (add the positive offset) to get it. Normally this will be // equal to rs1, but pointer masking can change that. - handle_mem_exception(vaddr - negative_offset, e); - RETIRE_FAIL + RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)) } } } @@ -110,8 +109,6 @@ function clause execute(RISCV_ZICBOM(cbop, rs1)) = process_clean_inval(rs1, cbop), CBO_INVAL if cbo_inval_enabled(cur_privilege) => process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH), - _ => { - handle_illegal(); - RETIRE_FAIL - }, + _ => + RETIRE_FAIL(Illegal_Instruction()) } diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail index 9dd55cdd2..5f3527828 100644 --- a/model/riscv_insts_zicboz.sail +++ b/model/riscv_insts_zicboz.sail @@ -32,7 +32,7 @@ function clause execute(RISCV_ZICBOZ(rs1)) = { let negative_offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val; match ext_data_get_addr(rs1, negative_offset, Write(Data), cache_block_size) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), Ext_DataAddr_OK(vaddr) => { // "An implementation may update the bytes in any order and with any granularity // and atomicity, including individual bytes." @@ -43,15 +43,15 @@ function clause execute(RISCV_ZICBOZ(rs1)) = { // was encoded in the instruction. We subtract the negative offset // (add the positive offset) to get it. Normally this will be // equal to rs1, but pointer masking can change that. - TR_Failure(e, _) => { handle_mem_exception(vaddr - negative_offset, e); RETIRE_FAIL }, + TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)), TR_Address(paddr, _) => { match mem_write_ea(paddr, cache_block_size, false, false, false) { - Err(e) => { handle_mem_exception(vaddr - negative_offset, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)), Ok(_) => { match mem_write_value(paddr, cache_block_size, zeros(), false, false, false) { Ok(true) => RETIRE_SUCCESS, Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - Err(e) => { handle_mem_exception(vaddr - negative_offset, e); RETIRE_FAIL }, + Err(e) => RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)) } } } @@ -60,7 +60,6 @@ function clause execute(RISCV_ZICBOZ(rs1)) = { }, } } else { - handle_illegal(); - RETIRE_FAIL + RETIRE_FAIL(Illegal_Instruction()) } } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 86d9415a9..0237316c7 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -24,9 +24,9 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = { let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1); let is_CSR_Write = op == CSRRW | rs1 != zeros(); if not(check_CSR(csr, cur_privilege, is_CSR_Write)) - then { handle_illegal(); RETIRE_FAIL } + then RETIRE_FAIL(Illegal_Instruction()) else if not(ext_check_CSR(csr, cur_privilege, is_CSR_Write)) - then { ext_check_CSR_fail(); RETIRE_FAIL } + then RETIRE_FAIL(Ext_CSR_Check_Failure()) else { /* CSRRW should not generate read side-effects if rd == 0 */ let is_CSR_Read = not(op == CSRRW & rd == zeros()); diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 69ae789b2..d2fae9198 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -18,15 +18,12 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { let t : xlenbits = X(rs1) + sign_extend(imm); /* Extensions get the first checks on the prospective target address. */ match ext_control_check_addr(t) { - Ext_ControlAddr_Error(e) => { - ext_handle_control_check_error(e); - RETIRE_FAIL - }, + Ext_ControlAddr_Error(e) => + RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), Ext_ControlAddr_OK(addr) => { let target = [virtaddr_bits(addr) with 0 = bitzero]; /* clear addr[0] */ if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca)) then { - handle_mem_exception(addr, E_Fetch_Addr_Align()); - RETIRE_FAIL + RETIRE_FAIL(Memory_Exception(addr, E_Fetch_Addr_Align())) } else { X(rd) = get_next_pc(); set_next_pc(target); diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 50d2116a9..8ba22006c 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -446,7 +446,7 @@ function tick_platform() -> unit = { /* Platform-specific handling of instruction faults */ -function handle_illegal() -> unit = { +function handle_illegal(instbits: xlenbits) -> unit = { let info = if plat_mtval_has_illegal_inst_bits () then Some(instbits) else None(); diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index d8b21d716..a4b5a9eca 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -11,9 +11,6 @@ register PC : xlenbits register nextPC : xlenbits -/* internal state to hold instruction bits for faulting instructions */ -register instbits : xlenbits - /* register file and accessors */ register x1 : regtype diff --git a/model/riscv_step.sail b/model/riscv_step.sail index d9e6423e5..3e8f7818c 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -8,6 +8,12 @@ /* The emulator fetch-execute-interrupt dispatch loop. */ +union Step = { + Step_Pending_Interrupt : (InterruptType, Privilege), + Step_Ext_Fetch_Failure : ext_fetch_addr_error, + Step_Execute : Retired(Retire_Failure) +} + /* returns whether to increment the step count in the trace */ function step(step_no : int) -> bool = { /* for step extensions */ @@ -23,31 +29,23 @@ function step(step_no : int) -> bool = { */ minstret_increment = should_inc_minstret(cur_privilege); - let (retired, stepped) : (Retired, bool) = + /* instruction bits for faulting instructions */ + var instbits : option(xlenbits) = None(); + + let (step_val, stepped) : (Step, bool) = match dispatchInterrupt(cur_privilege) { - Some(intr, priv) => { - if get_config_print_instr() - then print_bits("Handling interrupt: ", interruptType_to_bits(intr)); - handle_interrupt(intr, priv); - (RETIRE_FAIL, false) - }, + Some(intr, priv) => (Step_Pending_Interrupt(intr, priv), false), None() => { /* the extension hook interposes on the fetch result */ match ext_fetch_hook(fetch()) { /* extension error */ - F_Ext_Error(e) => { - ext_handle_fetch_check_error(e); - (RETIRE_FAIL, false) - }, + F_Ext_Error(e) => (Step_Ext_Fetch_Failure(e), false), /* standard error */ - F_Error(e, addr) => { - handle_mem_exception(virtaddr(addr), e); - (RETIRE_FAIL, false) - }, + F_Error(e, addr) => (Step_Execute(RETIRE_FAIL(Memory_Exception(virtaddr(addr), e))), false), /* non-error cases: */ F_RVC(h) => { sail_instr_announce(h); - instbits = zero_extend(h); + instbits = Some(zero_extend(h)); let ast = ext_decode_compressed(h); if get_config_print_instr() then { @@ -56,35 +54,63 @@ function step(step_no : int) -> bool = { /* check for RVC once here instead of every RVC execute clause. */ if extensionEnabled(Ext_Zca) then { nextPC = PC + 2; - (execute(ast), true) + (Step_Execute(execute(ast)), true) } else { - handle_illegal(); - (RETIRE_FAIL, true) + (Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true) } }, F_Base(w) => { sail_instr_announce(w); - instbits = zero_extend(w); + instbits = Some(zero_extend(w)); let ast = ext_decode(w); if get_config_print_instr() then { print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); }; nextPC = PC + 4; - (execute(ast), true) + (Step_Execute(execute(ast)), true) } } } }; - tick_pc(); + match step_val { + Step_Pending_Interrupt(intr, priv) => { + if get_config_print_instr() + then print_bits("Handling interrupt: ", interruptType_to_bits(intr)); + handle_interrupt(intr, priv) + }, + Step_Ext_Fetch_Failure(e) => { + ext_handle_fetch_check_error(e) + }, + Step_Execute(RETIRE_OK()) => { + retire_instruction() // update minstret + }, + Step_Execute(RETIRE_FAIL(failure)) => match failure { + // standard failures + Trap(priv, ctl, pc) => set_next_pc(exception_handler(priv, ctl, pc)), + Memory_Exception(vaddr, exc) => handle_mem_exception(vaddr, exc), + Illegal_Instruction() => match instbits { + None() => internal_error(__FILE__, __LINE__, "no instruction bits for illegal instruction"), + Some(instbits) => handle_illegal(instbits) + }, + Wait_For_Interrupt() => { + // This is currently treated as a nop that retires + // successfully. + platform_wfi(); + retire_instruction() + }, - /* update minstret */ - match retired { - RETIRE_SUCCESS => retire_instruction(), - RETIRE_FAIL => () + // failures from extensions + Ext_CSR_Check_Failure() => ext_check_CSR_fail(), + Ext_ControlAddr_Check_Failure(e) => ext_handle_control_check_error(e), + Ext_DataAddr_Check_Failure(e) => ext_handle_data_check_error(e), + Ext_XRET_Priv_Failure() => ext_fail_xret_priv () + } }; + tick_pc(); + /* for step extensions */ ext_post_step_hook(); diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 6d98064f3..238071018 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -107,9 +107,15 @@ function privLevel_to_str (p) = overload to_str = {privLevel_to_str} -/* enum denoting whether an executed instruction retires */ +/* Type denoting whether an executed instruction retires + * that is generic over the reasons why a retire might + * fail or be incomplete. + */ -enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} +union Retired ('a : Type) = { + RETIRE_OK : unit, + RETIRE_FAIL : 'a +} /* memory access types */ From 43bdc6431a7ac2e748b511802aaded9054f597b1 Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur <103736+pmundkur@users.noreply.github.com> Date: Mon, 24 Feb 2025 17:06:12 -0600 Subject: [PATCH 2/3] Implement a Wait state in the Sail stepper. The Wait state is exited on interrupts or if requested by the C emulator. The current implementation requests an immediate exit. --- c_emulator/riscv_sail.h | 8 +- c_emulator/riscv_sim.c | 9 +- model/riscv_step.sail | 186 ++++++++++++++++++++++++----------- model/riscv_step_common.sail | 18 ++++ model/riscv_sys_control.sail | 14 +++ 5 files changed, 173 insertions(+), 62 deletions(-) diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index da5aa9445..8ae102f6c 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -14,8 +14,14 @@ extern struct zMisa zmisa; void model_init(void); void model_fini(void); +enum zStepState { zSTEP_ACTIVE, zSTEP_WAIT }; +struct zstep_result { + enum zStepState zstate; + bool zstepped; +}; + unit zinit_model(unit); -bool zstep(sail_int); +struct zstep_result zstep(sail_int, bool); unit ztick_clock(unit); unit ztick_platform(unit); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 2d788867a..336c96311 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -692,7 +692,8 @@ void rvfi_send_trace(unsigned version) void run_sail(void) { - bool stepped; + struct zstep_result step_result; + bool exit_wait = true; bool diverged = false; /* initialize the step number */ @@ -800,7 +801,7 @@ void run_sail(void) sail_int sail_step; CREATE(sail_int)(&sail_step); CONVERT_OF(sail_int, mach_int)(&sail_step, step_no); - stepped = zstep(sail_step); + step_result = zstep(sail_step, exit_wait); if (have_exception) goto step_exception; flush_logs(); @@ -812,13 +813,13 @@ void run_sail(void) sail_int sail_step; CREATE(sail_int)(&sail_step); CONVERT_OF(sail_int, mach_int)(&sail_step, step_no); - stepped = zstep(sail_step); + step_result = zstep(sail_step, exit_wait); if (have_exception) goto step_exception; flush_logs(); KILL(sail_int)(&sail_step); } - if (stepped) { + if (step_result.zstepped) { if (config_print_step) { fprintf(trace_log, "\n"); } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 3e8f7818c..be9ad2fca 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -8,14 +8,117 @@ /* The emulator fetch-execute-interrupt dispatch loop. */ +register step_state : StepState + +function init_stepper() -> unit = { + step_state = STEP_ACTIVE; +} + +// Checks if the retire returned by the execution of an instruction +// counts as a step. +function does_executed_retire_step(r : Retired(Retire_Failure)) -> bool = + match r { + RETIRE_OK() => true, + RETIRE_FAIL(Illegal_Instruction()) => true, + RETIRE_FAIL(Memory_Exception(_)) => true, + RETIRE_FAIL(Trap(_)) => true, + + // do not step if a wait instruction executed. + RETIRE_FAIL(Wait_For_Interrupt()) => false, + + // retires from extensions + RETIRE_FAIL(Ext_ControlAddr_Check_Failure(_)) => true, + RETIRE_FAIL(Ext_DataAddr_Check_Failure(_)) => true, + RETIRE_FAIL(Ext_CSR_Check_Failure()) => true, + RETIRE_FAIL(Ext_XRET_Priv_Failure(_)) => true, +} + union Step = { Step_Pending_Interrupt : (InterruptType, Privilege), Step_Ext_Fetch_Failure : ext_fetch_addr_error, - Step_Execute : Retired(Retire_Failure) + Step_Execute : Retired(Retire_Failure), + Step_Waiting : unit +} + +function step_wait_state(step_no : int, exit_wait : bool) -> (Step, bool) = { + if wakeForInterrupt() then { + if get_config_print_instr() + then print_instr("interrupt exit from WAIT state at PC " ^ BitStr(PC)); + + step_state = STEP_ACTIVE; + // The waiting instruction retires successfully. The + // pending interrupts will be handled in the next step. + (Step_Execute(RETIRE_OK()), true) + } else if exit_wait then { + // There are no pending interrupts; transition out of the Wait + // as instructed. + if get_config_print_instr() + then print_instr("forced exit from WAIT state at PC " ^ BitStr(PC)); + + step_state = STEP_ACTIVE; + // "When TW=1, then if WFI is executed in any + // less-privileged mode, and it does not complete within an + // implementation-specific, bounded time limit, the WFI + // instruction causes an illegal-instruction exception." + if (cur_privilege == Machine | mstatus[TW] == 0b0) + then (Step_Execute(RETIRE_OK()), true) + else (Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true) + } else { + if get_config_print_instr() + then print_instr("remaining in WAIT state at PC " ^ BitStr(PC)); + (Step_Waiting(), false) + } +} + +function step_active_state(step_no: int, exit_wait : bool) -> ((Step, bool), option(xlenbits)) = { + match dispatchInterrupt(cur_privilege) { + Some(intr, priv) => ((Step_Pending_Interrupt(intr, priv), false), None()), + None() => match ext_fetch_hook(fetch()) { + /* extension error */ + F_Ext_Error(e) => ((Step_Ext_Fetch_Failure(e), false), None()), + /* standard error */ + F_Error(e, addr) => (((Step_Execute(RETIRE_FAIL(Memory_Exception(virtaddr(addr), e)))), false), None()), + /* non-error cases: */ + F_RVC(h) => { + sail_instr_announce(h); + let instbits : option(xlenbits) = Some(zero_extend(h)); + let ast = ext_decode_compressed(h); + if get_config_print_instr() + then { + print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); + }; + /* check for RVC once here instead of every RVC execute clause. */ + if extensionEnabled(Ext_Zca) then { + nextPC = PC + 2; + let r = execute(ast); + ((Step_Execute(r), does_executed_retire_step(r)), instbits) + } else { + ((Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true), instbits) + } + }, + F_Base(w) => { + sail_instr_announce(w); + let instbits : option(xlenbits) = Some(zero_extend(w)); + let ast = ext_decode(w); + if get_config_print_instr() + then { + print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); + }; + nextPC = PC + 4; + let r = execute(ast); + ((Step_Execute(r), does_executed_retire_step(r)), instbits) + } + } + } } -/* returns whether to increment the step count in the trace */ -function step(step_no : int) -> bool = { +// The `step` function is the main interface to the non-Sail +// harness. It receives the current step number (which numbers the +// active or wait step), and whether it should exit a wait state. +// It returns whether the Sail emulator executed a step, and the +// stepper state at the end of the step. + +function step(step_no : int, exit_wait : bool) -> step_result = { /* for step extensions */ ext_pre_step_hook(); @@ -29,49 +132,10 @@ function step(step_no : int) -> bool = { */ minstret_increment = should_inc_minstret(cur_privilege); - /* instruction bits for faulting instructions */ - var instbits : option(xlenbits) = None(); - - let (step_val, stepped) : (Step, bool) = - match dispatchInterrupt(cur_privilege) { - Some(intr, priv) => (Step_Pending_Interrupt(intr, priv), false), - None() => { - /* the extension hook interposes on the fetch result */ - match ext_fetch_hook(fetch()) { - /* extension error */ - F_Ext_Error(e) => (Step_Ext_Fetch_Failure(e), false), - /* standard error */ - F_Error(e, addr) => (Step_Execute(RETIRE_FAIL(Memory_Exception(virtaddr(addr), e))), false), - /* non-error cases: */ - F_RVC(h) => { - sail_instr_announce(h); - instbits = Some(zero_extend(h)); - let ast = ext_decode_compressed(h); - if get_config_print_instr() - then { - print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); - }; - /* check for RVC once here instead of every RVC execute clause. */ - if extensionEnabled(Ext_Zca) then { - nextPC = PC + 2; - (Step_Execute(execute(ast)), true) - } else { - (Step_Execute(RETIRE_FAIL(Illegal_Instruction())), true) - } - }, - F_Base(w) => { - sail_instr_announce(w); - instbits = Some(zero_extend(w)); - let ast = ext_decode(w); - if get_config_print_instr() - then { - print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); - }; - nextPC = PC + 4; - (Step_Execute(execute(ast)), true) - } - } - } + let ((step_val, stepped), instbits) : ((Step, bool), option(xlenbits)) = + match step_state { + STEP_WAIT => (step_wait_state(step_no, exit_wait), None()), + STEP_ACTIVE => step_active_state(step_no, exit_wait) }; match step_val { @@ -83,7 +147,11 @@ function step(step_no : int) -> bool = { Step_Ext_Fetch_Failure(e) => { ext_handle_fetch_check_error(e) }, + Step_Waiting() => { + assert(step_state == STEP_WAIT, "cannot be Waiting in a non-Wait state"); + }, Step_Execute(RETIRE_OK()) => { + assert(step_state == STEP_ACTIVE); retire_instruction() // update minstret }, Step_Execute(RETIRE_FAIL(failure)) => match failure { @@ -95,12 +163,11 @@ function step(step_no : int) -> bool = { Some(instbits) => handle_illegal(instbits) }, Wait_For_Interrupt() => { - // This is currently treated as a nop that retires - // successfully. - platform_wfi(); - retire_instruction() + // Transition into the wait state. + if get_config_print_instr() + then print_instr("entering WAIT state at PC " ^ BitStr(PC)); + step_state = STEP_WAIT }, - // failures from extensions Ext_CSR_Check_Failure() => ext_check_CSR_fail(), Ext_ControlAddr_Check_Failure(e) => ext_handle_control_check_error(e), @@ -109,12 +176,14 @@ function step(step_no : int) -> bool = { } }; - tick_pc(); + if step_state != STEP_WAIT then { + tick_pc(); - /* for step extensions */ - ext_post_step_hook(); + /* for step extensions */ + ext_post_step_hook(); + }; - stepped + struct { state = step_state, stepped } } function loop () : unit -> unit = { @@ -122,8 +191,10 @@ function loop () : unit -> unit = { var i : int = 0; var step_no : int = 0; while not(htif_done) do { - let stepped = step(step_no); - if stepped then { + // This standalone loop always exits immediately out of waiting + // states. + let step_result = step(step_no, true); + if step_result.stepped then { step_no = step_no + 1; if get_config_print_instr() then { print_step() @@ -161,5 +232,6 @@ function reset() -> unit = { // Initialize model state. This is only called once; not for every chip reset. function init_model() -> unit = { init_platform(); + init_stepper(); reset(); } diff --git a/model/riscv_step_common.sail b/model/riscv_step_common.sail index 5384e5b50..431a9009c 100644 --- a/model/riscv_step_common.sail +++ b/model/riscv_step_common.sail @@ -6,6 +6,24 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +// The state of the emulator. +// +// The RISC-V hart could either be active (fetching and executing +// instructions) or waiting (e.g. for an interrupt). The transition +// from `active` to `wait` occurs on instructions like WFI. The +// transition from `wait` to `active` can occur if (i) the hart +// detects an interrupt, or (ii) if the external non-Sail emulator +// harness indicates that the waiting instruction should be retired +// (as a nop). + +enum StepState = {STEP_ACTIVE, STEP_WAIT} + +// The return type of the `step` function. +struct step_result = { + state : StepState, + stepped : bool +} + /* The result of a fetch, which includes any possible error * from an extension that interposes on the fetch operation. */ diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ead87d08c..8bfb99359 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -129,6 +129,8 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = { * * We don't use the lowered views of {xie,xip} here, since the spec * allows for example the M_Timer to be delegated to the S-mode. + * + * This is used when the hart is in the Active state. */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { // mideleg can only be non-zero if we support Supervisor mode. @@ -145,6 +147,18 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { else None() } +/* Check if a locally enabled interrupt is pending. + * + * This does not examine the global enable bits (MIE and SIE in + * mstatus) and their delegation in mideleg. It does honor the + * local interrupt enables in mie. + * + * This is used when the hart is in the Waiting state. + */ +function wakeForInterrupt() -> bool = { + (mip.bits & mie.bits) != zeros() +} + /* Examine the current interrupt state and return an interrupt to be * * handled (if any), and the privilege it should be handled at. */ From a0d239332c32fff1197c56b2433f425dee10eb4b Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur <103736+pmundkur@users.noreply.github.com> Date: Mon, 17 Feb 2025 11:27:47 -0600 Subject: [PATCH 3/3] Use the exposed Wait state in the C emulator to implement a wait loop. This adds an option to configure the maximum steps to remain in the Wait state. This is currently only used for WFI, but the basic mechanism can be re-used for adding WRS.{STO, NTO} in the future. --- c_emulator/riscv_sim.c | 39 ++++++++++++++++++++++++++++++++------- 1 file changed, 32 insertions(+), 7 deletions(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 336c96311..59ee07153 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -54,6 +54,7 @@ enum { OPT_ENABLE_ZICBOZ, OPT_ENABLE_SSTC, OPT_CACHE_BLOCK_SIZE, + OPT_MAX_WAIT_STEPS, }; static bool do_show_times = false; @@ -72,6 +73,8 @@ static int rvfi_dii_port; static int rvfi_dii_sock; #endif +int max_wait_steps = 0; + char *sig_file = NULL; uint64_t mem_sig_start = 0; uint64_t mem_sig_end = 0; @@ -151,6 +154,7 @@ static struct option options[] = { {"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM }, {"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ }, {"cache-block-size", required_argument, 0, OPT_CACHE_BLOCK_SIZE }, + {"max-wait-steps", required_argument, 0, OPT_MAX_WAIT_STEPS }, #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c' }, #endif @@ -240,6 +244,7 @@ static int process_args(int argc, char **argv) uint64_t pmp_count = 0; uint64_t pmp_grain = 0; uint64_t block_size_exp = 0; + int wait_steps = 0; while (true) { c = getopt_long(argc, argv, "a" @@ -412,6 +417,15 @@ static int process_args(int argc, char **argv) block_size_exp, 1 << block_size_exp); rv_cache_block_size_exp = block_size_exp; break; + case OPT_MAX_WAIT_STEPS: + wait_steps = atoi(optarg); + if (wait_steps < 0) { + fprintf(stderr, "invalid max-wait-steps '%s' provided.\n", optarg); + exit(1); + } + fprintf(stderr, "setting max-wait-states to %d steps.\n", wait_steps); + max_wait_steps = wait_steps; + break; case 'x': fprintf(stderr, "enabling Zfinx support.\n"); rv_enable_zfinx = true; @@ -693,12 +707,13 @@ void rvfi_send_trace(unsigned version) void run_sail(void) { struct zstep_result step_result; - bool exit_wait = true; + bool exit_wait = (max_wait_steps > 0) ? false : true; bool diverged = false; /* initialize the step number */ mach_int step_no = 0; int insn_cnt = 0; + int wait_steps = 0; #ifdef RVFI_DII bool need_instr = true; #endif @@ -819,13 +834,23 @@ void run_sail(void) flush_logs(); KILL(sail_int)(&sail_step); } - if (step_result.zstepped) { - if (config_print_step) { - fprintf(trace_log, "\n"); + switch (step_result.zstate) { + case zSTEP_WAIT: + if (++wait_steps >= max_wait_steps) + exit_wait = true; + break; + case zSTEP_ACTIVE: + wait_steps = 0; + exit_wait = (max_wait_steps > 0) ? false : true; + if (step_result.zstepped) { + if (config_print_step) { + fprintf(trace_log, "\n"); + } + step_no++; + insn_cnt++; + total_insns++; } - step_no++; - insn_cnt++; - total_insns++; + break; } if (do_show_times && (total_insns & 0xfffff) == 0) {