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/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..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; @@ -692,12 +706,14 @@ void rvfi_send_trace(unsigned version) void run_sail(void) { - bool stepped; + struct zstep_result step_result; + 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 @@ -800,7 +816,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,19 +828,29 @@ 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 (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) { 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..be9ad2fca 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -8,8 +8,117 @@ /* The emulator fetch-execute-interrupt dispatch loop. */ -/* returns whether to increment the step count in the trace */ -function step(step_no : int) -> bool = { +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_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) + } + } + } +} + +// 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(); @@ -23,72 +132,58 @@ function step(step_no : int) -> bool = { */ minstret_increment = should_inc_minstret(cur_privilege); - let (retired, stepped) : (Retired, bool) = - match dispatchInterrupt(cur_privilege) { - Some(intr, priv) => { + 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 { + 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_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 { + // 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() => { + // Transition into the wait state. if get_config_print_instr() - then print_bits("Handling interrupt: ", interruptType_to_bits(intr)); - handle_interrupt(intr, priv); - (RETIRE_FAIL, false) + then print_instr("entering WAIT state at PC " ^ BitStr(PC)); + step_state = STEP_WAIT }, - 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) - }, - /* standard error */ - F_Error(e, addr) => { - handle_mem_exception(virtaddr(addr), e); - (RETIRE_FAIL, false) - }, - /* non-error cases: */ - F_RVC(h) => { - sail_instr_announce(h); - instbits = 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; - (execute(ast), true) - } else { - handle_illegal(); - (RETIRE_FAIL, true) - } - }, - F_Base(w) => { - sail_instr_announce(w); - instbits = 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) - } - } - } - }; + // 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(); + if step_state != STEP_WAIT then { + tick_pc(); - /* update minstret */ - match retired { - RETIRE_SUCCESS => retire_instruction(), - RETIRE_FAIL => () + /* for step extensions */ + ext_post_step_hook(); }; - /* for step extensions */ - ext_post_step_hook(); - - stepped + struct { state = step_state, stepped } } function loop () : unit -> unit = { @@ -96,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() @@ -135,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. */ 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 */