Assertions

Immediate Assertions

Name	Kind	Description
uvm_pkg::uvm_component_name_check_visitor.[anonymous]	assert	(compiled_regex != null)
uvm_pkg::uvm_reg_map.[anonymous]	assert	$cast(seq, o)
uvm_pkg::uvm_reg_map.[anonymous]	assert	$cast(seq, o)
prim_count.AssertConnected_A	assert	((unused_assert_connected === 1'b1) || ! EnableAlertTriggerSVA)
prim_ram_1p_adv.CannotHaveEccAndParity_A	assert	! (EnableParity && EnableECC)
prim_ram_1p_adv.SecDecWidth_A	assert	check supported widths (Width inside {16, 32})
prim_ram_1p_adv.WidthNeedsToBeByteAligned_A	assert	((Width % 8) == 0)
prim_ram_1p_adv.ParityNeedsByteWriteMask_A	assert	(DataBitsPerMask == 8)
prim_ram_1p_scr.DepthPow2Check_A	assert	The depth needs to be a power of 2 in case address scrambling is turned on ((NumAddrScrRounds <= '0) || ((2 ** $clog2(Depth)) == Depth))
prim_ram_1p_scr.DiffWidthMinimum_A	assert	(DiffWidth >= 4)
prim_ram_1p_scr.DiffWidthWithParity_A	assert	((EnableParity && (DiffWidth == 8)) || ! EnableParity)
prim_generic_ram_1p.DataBitsPerMaskCheck_A	assert	Width must be fully divisible by DataBitsPerMask ((Width % DataBitsPerMask) == 0)
prim_lfsr.MinLfsrWidth_A	assert	check that the most significant bit of polynomial is 1 (LfsrDw >= ($low(LFSR_COEFFS) + LUT_OFF))
prim_lfsr.MaxLfsrWidth_A	assert	(LfsrDw <= ($high(LFSR_COEFFS) + LUT_OFF))
prim_lfsr.DefaultSeedNzCheck_A	assert	check that seed is not all-zero | DefaultSeedLocal
prim_lfsr.MinLfsrWidth_A	assert	check that the most significant bit of polynomial is 1 (LfsrDw >= ($low(LFSR_COEFFS) + LUT_OFF))
prim_lfsr.MaxLfsrWidth_A	assert	(LfsrDw <= ($high(LFSR_COEFFS) + LUT_OFF))
prim_lfsr.DefaultSeedNzCheck_A	assert	check that seed is not all-ones ! & DefaultSeedLocal
prim_lfsr.UnknownLfsrType_A	assert	0
prim_lfsr.PermutationCheck_A	assert	All bit positions must be marked with 1. & lfsr_perm_test
prim_lfsr.InputWidth_A	assert	(LfsrDw >= EntropyDw)
prim_lfsr.OutputWidth_A	assert	(LfsrDw >= StateOutDw)
prim_lfsr.SboxByteAlign_A	assert	(((2 ** $clog2(LfsrDw)) == LfsrDw) && (LfsrDw >= 16))
prim_prince.SupportedWidths_A	assert	////////////// assertions // ////////////// (((DataWidth == 64) && (KeyWidth == 128)) || ((DataWidth == 32) && (KeyWidth == 64)))
prim_prince.SupportedNumRounds_A	assert	((NumRoundsHalf > 0) && (NumRoundsHalf < 6))
prim_onehot_check.NumSources_A	assert	///////////////////// Binary tree logic // ///////////////////// (OneHotWidth >= 1)
prim_onehot_check.AddrWidth_A	assert	(AddrWidth >= 1)
prim_onehot_check.AddrRange_A	assert	(OneHotWidth <= (2 ** AddrWidth))
prim_onehot_check.AddrImpliesEnable_A	assert	((AddrCheck && EnableCheck) || ! AddrCheck)
prim_onehot_check.AssertConnected_A	assert	((unused_assert_connected === 1'b1) || ! EnableAlertTriggerSVA)
ibex_cs_registers.PMPAddrRstLowBitsZero_A	assert	(PMPRstAddr[i][33 - PMPAddrWidth : 0] == '0)
ibex_icache.size_param_legal	assert	////////////// Assertions // ////////////// (IC_LINE_SIZE > 32)
ibex_icache.ecc_tag_param_legal	assert	ECC primitives will need to be changed for different sizes (IC_TAG_SIZE <= 27)
ibex_icache.ecc_data_param_legal	assert	(! ICacheECC || (BUS_SIZE == 32))
ibex_core.IbexMuBiSecureOnBottomBitSet	assert	Multi-bit fetch enable used when SecureIbex == 1. When SecureIbex == 0 only use the bottom-bit of fetch_enable_i. Ensure the multi-bit encoding has the bottom bit set for on and unset for off so IbexMuBiOn/IbexMuBiOff can be used without needing to know the value of SecureIbex. (IbexMuBiOn[0] == 1'b1)
ibex_core.IbexMuBiSecureOffBottomBitClear	assert	(IbexMuBiOff[0] == 1'b0)
ibex_core.IllegalParamSecure	assert	Certain parameter combinations are not supported ! (SecureIbex && (RV32M == RV32MNone))
ibex_top.DmHaltAddrInRange_A	assert	Parameter assertions ((DmHaltAddr & ~ DmAddrMask) == DmBaseAddr)
ibex_top.DmExceptionAddrInRange_A	assert	((DmExceptionAddr & ~ DmAddrMask) == DmBaseAddr)
pins_if.PullStrengthParamValid	assert	(PullStrength inside {"Weak", "Pull"})

Concurrent Assertions

Name	Kind	Description
prim_count.ClrNeverTrue_A	assert	disable iff((!rst_ni)!=='0)(clr_i !== 1'b1)
prim_count.SetNeverTrue_A	assert	disable iff((!rst_ni)!=='0)(set_i !== 1'b1)
prim_count.IncrNeverTrue_A	assert	disable iff((!rst_ni)!=='0)(incr_en_i !== 1'b1)
prim_count.DecrNeverTrue_A	assert	disable iff((!rst_ni)!=='0)(decr_en_i !== 1'b1)
prim_count.CntNext_A	assert	Cnt next disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(rst_ni |=> ($past(! commit_i) || (cnt_o == $past(cnt_after_commit_o))))
prim_count.ClrFwd_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(((rst_ni && commit_i) && clr_i) |=> ((cnt_o == ResetValue) && (cnt_q[1] == ({Width{1'b1}} - ResetValue))))
prim_count.SetFwd_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && commit_i) && set_i) && ! clr_i) |=> ((cnt_o == $past(set_cnt_i)) && (cnt_q[1] == ({Width{1'b1}} - $past(set_cnt_i)))))
prim_count.IncrDecrUpDnCnt_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && decr_en_i) && ! (clr_i || set_i)) |=> ($stable(cnt_o) && $stable(cnt_q[1])))
prim_count.IncrUpCnt_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && ! ((clr_i || set_i) || decr_en_i)) && commit_i) |=> (cnt_o == min(($past(cnt_o) + $past({2'b0, step_i})), {2'b0, {Width{1'b1}}})))
prim_count.IncrDnCnt_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && ! ((clr_i || set_i) || decr_en_i)) && commit_i) |=> (cnt_q[1] == max(($past((signed ' {2'b0, cnt_q[1]})) - $past({2'b0, step_i})), '0)))
prim_count.UpCntIncrStable_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(((incr_en_i && ! ((clr_i || set_i) || decr_en_i)) && (cnt_o == {Width{1'b1}})) |=> $stable(cnt_o))
prim_count.DnCntIncrStable_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && ! ((clr_i || set_i) || decr_en_i)) && (cnt_q[1] == '0)) |=> $stable(cnt_q[1]))
prim_count.DecrUpCnt_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && decr_en_i) && ! ((clr_i || set_i) || incr_en_i)) && commit_i) |=> (cnt_o == max(($past((signed ' {2'b0, cnt_o})) - $past({2'b0, step_i})), '0)))
prim_count.DecrDnCnt_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && decr_en_i) && ! ((clr_i || set_i) || incr_en_i)) && commit_i) |=> (cnt_q[1] == min(($past(cnt_q[1]) + $past({2'b0, step_i})), {2'b0, {Width{1'b1}}})))
prim_count.UpCntDecrStable_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(((decr_en_i && ! ((clr_i || set_i) || incr_en_i)) && (cnt_o == '0)) |=> $stable(cnt_o))
prim_count.DnCntDecrStable_A	assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && decr_en_i) && ! ((clr_i || set_i) || incr_en_i)) && (cnt_q[1] == {Width{1'b1}})) |=> $stable(cnt_q[1]))
prim_count.ChangeBackward_A	assert	A backwards check for count changes. This asserts that the count only changes if one of the inputs that should tell it to change (clear, set, increment, decrement) does so. disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(rst_ni ## 1 (($changed(cnt_o) && $changed(cnt_q[1])) |-> $past(((clr_i || set_i) || (commit_i && (incr_en_i || decr_en_i))))))
prim_count.CntErrReported_A	assert	Check that count errors are reported properly in err_o disable iff((!rst_ni)!=='0)(((cnt_q[1] + cnt_q[0]) != {Width{1'b1}}) == err_o)
prim_ram_1p_adv.OnlyWordWritePossibleWithEccPortA_A	assert	the wmask is constantly set to 1 in this case disable iff((!rst_ni)!=='0)(req_i |-> (wmask_i == {Width{1'b1}}))
prim_generic_ram_1p.MaskCheck_A	assert	Ensure that all mask bits within a group have the same value for a write disable iff(('0)!=='0)((req_i && write_i) |-> (wmask_i[k * DataBitsPerMask +: DataBitsPerMask] inside {{DataBitsPerMask{1'b1}}, '0}))
prim_generic_clock_mux2.selKnown0	assert	make sure sel is never X (including during reset) need to use ##1 as this could break with inverted clocks that start with a rising edge at the beginning of the simulation. disable iff((0)!=='0)(## 1 ! $isunknown(sel_i))
prim_generic_clock_mux2.selKnown1	assert	disable iff((0)!=='0)(## 1 ! $isunknown(sel_i))
prim_lfsr.SboxPermutationCheck_A	assert	All bit positions must be marked with 1. disable iff((!rst_ni)!=='0)& sbox_perm_test
prim_lfsr.DataKnownO_A	assert	///////////////////// shared assertions // ///////////////////// disable iff((!rst_ni)!=='0)! $isunknown(state_o)
prim_lfsr.NextStateCheck_A	assert	check whether next state is computed correctly we shift the assertion by one clock cycle (##1) in order to avoid erroneous SVA triggers right after reset deassertion in cases where the precondition is true throughout the reset. this can happen since the disable_iff evaluates using unsampled values, meaning that the assertion may already read rst_ni == 1 on an active clock edge while the flops in the design have not yet changed state. disable iff((!rst_ni)!=='0)(## 1 ((lfsr_en_i && ! seed_en_i) |=> (lfsr_q == compute_next_state(coeffs, $past(entropy_i), $past(lfsr_q)))))
prim_lfsr.CoeffCheck_A	assert	MSB must be one in any case disable iff((!rst_ni)!=='0)coeffs[LfsrDw - 1]
prim_lfsr.OutputKnown_A	assert	output check disable iff((!rst_ni)!=='0)! $isunknown(state_o)
prim_lfsr.OutputCheck_A	assert	disable iff((!rst_ni)!=='0)(state_o == (StateOutDw ' lfsr_q))
prim_lfsr.NoLockups_A	assert	if no external input changes the lfsr state, a lockup must not occur (by design) `ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni) disable iff((!rst_ni)!=='0)(((lfsr_en_i && ! entropy_i) && ! seed_en_i) |=> ! lockup)
prim_lfsr.ExtDefaultSeedInputCheck_A	assert	check that external seed is correctly loaded into the state rst_ni is used directly as part of the pre-condition since the usage of rst_ni in disable_iff is unsampled. See #1985 for more details disable iff((!rst_ni)!=='0)((seed_en_i && rst_ni) |=> (lfsr_q == $past(seed_i)))
prim_lfsr.LfsrLockupCheck_A	assert	check that a stuck LFSR is correctly reseeded disable iff((!rst_ni)!=='0)(((lfsr_en_i && lockup) && ! seed_en_i) |=> ! lockup)
prim_lfsr.MaximalLengthCheck0_A	assert	disable iff((!rst_ni||perturbed_q)!=='0)((cnt_q == 0) |-> (lfsr_q == DefaultSeedLocal))
prim_lfsr.MaximalLengthCheck1_A	assert	disable iff((!rst_ni||perturbed_q)!=='0)((cnt_q != 0) |-> (lfsr_q != DefaultSeedLocal))
prim_onehot_check.Onehot0Check_A	assert	disable iff((!rst_ni)!=='0)(! $onehot0(oh_i) |-> err_o)
prim_onehot_check.EnableCheck_A	assert	disable iff((!rst_ni)!=='0)((| oh_i != en_i) |-> err_o)
prim_onehot_check.EnableCheck_A	assert	disable iff((!rst_ni)!=='0)((! en_i && | oh_i) |-> err_o)
prim_onehot_check.AddrCheck_A	assert	disable iff((!rst_ni)!=='0)((oh_i[addr_i] != | oh_i) |-> err_o)
prim_onehot_mux.SelIsOnehot_A	assert	disable iff((!rst_ni)!=='0)$onehot0(sel_i)
ibex_branch_predict.BranchInsTypeOneHot	assert	disable iff((!rst_ni)!=='0)(fetch_valid_i |-> $onehot0({instr_j, instr_b, instr_cj, instr_cb}))
ibex_compressed_decoder.IbexInstrValidKnown	assert	The valid_i signal used to gate below assertions must be known. disable iff((!rst_ni)!=='0)! $isunknown(valid_i)
ibex_compressed_decoder.IbexInstrLSBsKnown	assert	Selectors must be known/valid. disable iff((!rst_ni)!=='0)(valid_i |-> ! $isunknown(instr_i[1 : 0]))
ibex_compressed_decoder.IbexC0Known1	assert	disable iff((!rst_ni)!=='0)((valid_i && (instr_i[1 : 0] == 2'b00)) |-> ! $isunknown(instr_i[15 : 13]))
ibex_compressed_decoder.IbexC1Known1	assert	disable iff((!rst_ni)!=='0)((valid_i && (instr_i[1 : 0] == 2'b01)) |-> ! $isunknown(instr_i[15 : 13]))
ibex_compressed_decoder.IbexC1Known2	assert	disable iff((!rst_ni)!=='0)(((valid_i && (instr_i[1 : 0] == 2'b01)) && (instr_i[15 : 13] == 3'b100)) |-> ! $isunknown(instr_i[11 : 10]))
ibex_compressed_decoder.IbexC1Known3	assert	disable iff((!rst_ni)!=='0)((((valid_i && (instr_i[1 : 0] == 2'b01)) && (instr_i[15 : 13] == 3'b100)) && (instr_i[11 : 10] == 2'b11)) |-> ! $isunknown({instr_i[12], instr_i[6 : 5]}))
ibex_compressed_decoder.IbexC2Known1	assert	disable iff((!rst_ni)!=='0)((valid_i && (instr_i[1 : 0] == 2'b10)) |-> ! $isunknown(instr_i[15 : 13]))
ibex_controller.IllegalInsnOnlyIfInsnValid	assert	disable iff((!rst_ni)!=='0)(illegal_insn_i |-> instr_valid_i)
ibex_controller.IbexExceptionPrioOnehot	assert	disable iff((!rst_ni)!=='0)(((ctrl_fsm_cs == FLUSH) & exc_req_q) |-> $onehot({instr_fetch_err_prio, illegal_insn_prio, ecall_insn_prio, ebrk_insn_prio, store_err_prio, load_err_prio}))
ibex_controller.PipeEmptyOnIrq	assert	disable iff((!rst_ni)!=='0)(((ctrl_fsm_cs != IRQ_TAKEN) & (ctrl_fsm_ns == IRQ_TAKEN)) |-> (~ instr_valid_i & ready_wb_i))
ibex_controller.AlwaysInstrClearOnMispredict	assert	////////////// Assertions // ////////////// disable iff((!rst_ni)!=='0)(nt_branch_mispredict_o |-> instr_valid_clear_o)
ibex_controller.IbexCtrlStateValid	assert	Selectors must be known/valid. disable iff((!rst_ni)!=='0)(ctrl_fsm_cs inside {RESET, BOOT_SET, WAIT_SLEEP, SLEEP, FIRST_FETCH, DECODE, FLUSH, IRQ_TAKEN, DBG_TAKEN_IF, DBG_TAKEN_ID})
ibex_controller.IbexPipelineFlushOnChangingDebugMode	assert	If entering or exiting debug mode, the pipeline must be flushed. This is because Ibex currently does not support some of the pipeline stages being in debug mode; either all or none of the pipeline stages must be in debug mode. As flush_id_o only affects the ID/EX stage but does not prevent a fetched instruction from proceeding to ID/EX the next cycle, the assertion additionally requires pc_set_o, which sets the PC in the IF stage to a new value, hence preventing a fetched instruction from proceeding to the ID/EX stage in the next cycle. disable iff((!rst_ni)!=='0)((debug_mode_d != debug_mode_q) |-> (flush_id_o & pc_set_o))
ibex_csr.IbexCSREnValid	assert	disable iff((!rst_ni)!=='0)! $isunknown(wr_en_i)
ibex_cs_registers.IbexCsrOpEnRequiresAccess	assert	////////////// Assertions // ////////////// disable iff((!rst_ni)!=='0)(csr_op_en_i |-> csr_access_i)
ibex_decoder.IbexRegImmAluOpKnown	assert	Selectors must be known/valid. disable iff((!rst_ni)!=='0)((opcode == OPCODE_OP_IMM) |-> ! $isunknown(instr[14 : 12]))
ibex_wb_stage.RFWriteFromOneSourceOnly	assert	disable iff((!rst_ni)!=='0)$onehot0(rf_wdata_wb_mux_we)
ibex_id_stage.IbexImmBMuxSelValid	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> (imm_b_mux_sel inside {IMM_B_I, IMM_B_S, IMM_B_U, IMM_B_INCR_PC, IMM_B_INCR_ADDR}))
ibex_id_stage.IbexImmBMuxSelValid	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> (imm_b_mux_sel inside {IMM_B_I, IMM_B_S, IMM_B_B, IMM_B_U, IMM_B_J, IMM_B_INCR_PC, IMM_B_INCR_ADDR}))
ibex_id_stage.NeverDoubleBranch	assert	Holding branch_set/jump_set high for more than one cycle should not cause a functional issue. However it could generate needless prefetch buffer flushes and instruction fetches. The ID/EX designs ensures that this never happens for non-predicted branches. disable iff((!rst_ni)!=='0)((branch_set & ~ instr_bp_taken_i) |=> ~ branch_set)
ibex_id_stage.NeverDoubleJump	assert	disable iff((!rst_ni)!=='0)((jump_set & ~ instr_bp_taken_i) |=> ~ jump_set)
ibex_id_stage.StallIDIfMulticycle	assert	disable iff((!rst_ni)!=='0)(((id_fsm_q == FIRST_CYCLE) & (id_fsm_d == MULTI_CYCLE)) |-> stall_id)
ibex_id_stage.IllegalInsnStallMustBeMemStall	assert	Generally illegal instructions have no reason to stall, however they must still stall waiting for outstanding memory requests so exceptions related to them take priority over the illegal instruction exception. disable iff((!rst_ni)!=='0)((illegal_insn_o & stall_id) |-> (stall_mem & ~ ((((stall_ld_hz | stall_multdiv) | stall_jump) | stall_branch) | stall_alu)))
ibex_id_stage.IbexExecutingSpecIfExecuting	assert	disable iff((!rst_ni)!=='0)(instr_executing |-> instr_executing_spec)
ibex_id_stage.IbexStallIfValidInstrNotExecuting	assert	disable iff((!rst_ni)!=='0)(((instr_valid_i & ~ instr_kill) & ~ instr_executing) |-> stall_id)
ibex_id_stage.IbexCannotRetireWithPendingExceptions	assert	disable iff((!rst_ni)!=='0)(instr_done |-> ~ (wb_exception | outstanding_memory_access))
ibex_id_stage.IbexStallMemNoRequest	assert	If we stall a load in ID for any reason, it must not make an LSU request (otherwide we might issue two requests for the same instruction) disable iff((!rst_ni)!=='0)(((instr_valid_i & lsu_req_dec) & ~ instr_done) |-> ~ lsu_req_done_i)
ibex_id_stage.IbexStallIfValidInstrNotExecuting	assert	disable iff((!rst_ni)!=='0)((((instr_valid_i & ~ instr_fetch_err_i) & ~ instr_executing) & controller_run) |-> stall_id)
ibex_id_stage.IbexAluOpMuxSelKnownKnownEnable	assert	Selectors must be known/valid. disable iff((!rst_ni)!=='0)! $isunknown(instr_valid_i)
ibex_id_stage.IbexAluOpMuxSelKnown	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> ! $isunknown(alu_op_a_mux_sel))
ibex_id_stage.IbexAluAOpMuxSelValid	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> (alu_op_a_mux_sel inside {OP_A_REG_A, OP_A_FWD, OP_A_CURRPC, OP_A_IMM}))
ibex_id_stage.IbexBTAluAOpMuxSelKnownKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(instr_valid_i)
ibex_id_stage.IbexBTAluAOpMuxSelKnown	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> ! $isunknown(bt_a_mux_sel))
ibex_id_stage.IbexBTAluAOpMuxSelValid	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> (bt_a_mux_sel inside {OP_A_REG_A, OP_A_CURRPC}))
ibex_id_stage.IbexBTAluBOpMuxSelKnownKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(instr_valid_i)
ibex_id_stage.IbexBTAluBOpMuxSelKnown	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> ! $isunknown(bt_b_mux_sel))
ibex_id_stage.IbexBTAluBOpMuxSelValid	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> (bt_b_mux_sel inside {IMM_B_I, IMM_B_B, IMM_B_J, IMM_B_INCR_PC}))
ibex_id_stage.IbexRegfileWdataSelValid	assert	disable iff((!rst_ni)!=='0)(instr_valid_i |-> (rf_wdata_sel inside {RF_WD_EX, RF_WD_CSR}))
ibex_id_stage.IbexWbStateKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown(id_fsm_q)
ibex_id_stage.IbexBranchDecisionValidKnownEnable	assert	Branch decision must be valid when jumping. disable iff((!rst_ni)!=='0)! $isunknown((instr_valid_i && ! (illegal_csr_insn_i || instr_fetch_err_i)))
ibex_id_stage.IbexBranchDecisionValid	assert	disable iff((!rst_ni)!=='0)((instr_valid_i && ! (illegal_csr_insn_i || instr_fetch_err_i)) |-> ! $isunknown(branch_decision_i))
ibex_id_stage.IbexIdInstrKnownKnownEnable	assert	Instruction delivered to ID stage can not contain X. disable iff((!rst_ni)!=='0)! $isunknown((instr_valid_i && ! (illegal_c_insn_i || instr_fetch_err_i)))
ibex_id_stage.IbexIdInstrKnown	assert	disable iff((!rst_ni)!=='0)((instr_valid_i && ! (illegal_c_insn_i || instr_fetch_err_i)) |-> ! $isunknown(instr_rdata_i))
ibex_id_stage.IbexIdInstrALUKnownKnownEnable	assert	Instruction delivered to ID stage can not contain X. disable iff((!rst_ni)!=='0)! $isunknown((instr_valid_i && ! (illegal_c_insn_i || instr_fetch_err_i)))
ibex_id_stage.IbexIdInstrALUKnown	assert	disable iff((!rst_ni)!=='0)((instr_valid_i && ! (illegal_c_insn_i || instr_fetch_err_i)) |-> ! $isunknown(instr_rdata_alu_i))
ibex_id_stage.IbexMulticycleEnableUnique	assert	Multicycle enable signals must be unique. disable iff((!rst_ni)!=='0)$onehot0({lsu_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec})
ibex_id_stage.IbexDuplicateInstrMatch	assert	Duplicated instruction flops must match === as DV environment can produce instructions with Xs in, so must use precise match that includes Xs disable iff((!rst_ni)!=='0)(instr_valid_i |-> (instr_rdata_i === instr_rdata_alu_i))
ibex_id_stage.IbexMoveToFirstCycleWhenIdReady	assert	Check that when ID stage is ready for next instruction FSM is in FIRST_CYCLE state the following cycle (when the new instructon may begin executing). disable iff((!rst_ni)!=='0)(id_in_ready_o |=> (id_fsm_q == FIRST_CYCLE))
ibex_icache.TagHitKnown	assert	Lookups in the tag ram should always give a known result disable iff((!rst_ni)!=='0)! $isunknown((lookup_valid_ic1 & tag_hit_ic1))
ibex_icache.TagInvalidKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown((lookup_valid_ic1 & tag_invalid_ic1))
ibex_if_stage.NoMispredBranch	assert	We should never see a mispredict and an incoming branch on the same cycle. The mispredict also cancels any predicted branch so overall branch_req must be low. disable iff((!rst_ni)!=='0)(nt_branch_mispredict_i |-> ~ branch_req)
ibex_if_stage.NoPredictSkid	assert	disable iff((!rst_ni)!=='0)(instr_skid_valid_q |-> ~ predict_branch_taken)
ibex_if_stage.NoPredictIllegal	assert	disable iff((!rst_ni)!=='0)(predict_branch_taken |-> ~ illegal_c_insn)
ibex_if_stage.IbexExcPcMuxKnown	assert	Selectors must be known/valid. disable iff((!rst_ni)!=='0)! $isunknown(exc_pc_mux_i)
ibex_if_stage.IbexPcMuxValid	assert	disable iff((!rst_ni)!=='0)(pc_set_i |-> (pc_mux_internal inside {PC_BOOT, PC_JUMP, PC_EXC, PC_ERET, PC_DRET, PC_BP}))
ibex_if_stage.MispredictOnlyImmediatelyAfterPredictedBranch	assert	Must only see mispredict after we've performed a predicted branch but before we've accepted any instruction (with fetch_ready & fetch_valid) that follows that predicted branch. disable iff((!rst_ni)!=='0)(nt_branch_mispredict_i |-> predicted_branch_live_q)
ibex_if_stage.CorrectPCOnMispredict	assert	Check that on mispredict we get the correct PC for the non-taken side of the branch when prefetch buffer/icache makes that PC available. disable iff((!rst_ni)!=='0)(((predicted_branch_live_q & mispredicted_d) & fetch_valid) |-> (fetch_addr == predicted_branch_nt_pc_q))
ibex_if_stage.MispredictSingleCycle	assert	Must not signal mispredict over multiple cycles but it's possible to have back to back mispredicts for different branches (core signals mispredict, prefetch buffer/icache immediate has not-taken side of the mispredicted branch ready, which itself is a predicted branch, following cycle core signal that that branch has mispredicted). disable iff((!rst_ni)!=='0)((nt_branch_mispredict_i & ~ (fetch_valid & fetch_ready)) |=> ~ nt_branch_mispredict_i)
ibex_if_stage.IbexPcMuxValid	assert	disable iff((!rst_ni)!=='0)(pc_set_i |-> (pc_mux_internal inside {PC_BOOT, PC_JUMP, PC_EXC, PC_ERET, PC_DRET}))
ibex_if_stage.IbexBootAddrUnaligned	assert	Boot address must be aligned to 256 bytes. disable iff((!rst_ni)!=='0)(boot_addr_i[7 : 0] == 8'h00)
ibex_if_stage.IbexInstrAddrUnknown	assert	Address must not contain X when request is sent. disable iff((!rst_ni)!=='0)(instr_req_o |-> ! $isunknown(instr_addr_o))
ibex_if_stage.IbexInstrAddrUnaligned	assert	Address must be word aligned when request is sent. disable iff((!rst_ni)!=='0)(instr_req_o |-> (instr_addr_o[1 : 0] == 2'b00))
ibex_load_store_unit.IbexDataTypeKnown	assert	Selectors must be known/valid. disable iff((!rst_ni)!=='0)((lsu_req_i | busy_o) |-> ! $isunknown(lsu_type_i))
ibex_load_store_unit.IbexDataOffsetKnown	assert	disable iff((!rst_ni)!=='0)((lsu_req_i | busy_o) |-> ! $isunknown(data_offset))
ibex_load_store_unit.IbexRDataOffsetQKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown(rdata_offset_q)
ibex_load_store_unit.IbexDataTypeQKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown(data_type_q)
ibex_load_store_unit.IbexLsuStateValid	assert	disable iff((!rst_ni)!=='0)(ls_fsm_cs inside {IDLE, WAIT_GNT_MIS, WAIT_RVALID_MIS, WAIT_GNT, WAIT_RVALID_MIS_GNTS_DONE})
ibex_load_store_unit.IbexDataAddrUnknown	assert	Address must not contain X when request is sent. disable iff((!rst_ni)!=='0)(data_req_o |-> ! $isunknown(data_addr_o))
ibex_load_store_unit.IbexDataAddrUnaligned	assert	Address must be word aligned when request is sent. disable iff((!rst_ni)!=='0)(data_req_o |-> (data_addr_o[1 : 0] == 2'b00))
ibex_multdiv_slow.IbexMultDivStateValid	assert	State must be valid. disable iff((!rst_ni)!=='0)(md_state_q inside {MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH})
ibex_multdiv_fast.DivEnKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown(div_en_internal)
ibex_multdiv_fast.MultEnKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown(mult_en_internal)
ibex_multdiv_fast.MultDivEnKnown	assert	disable iff((!rst_ni)!=='0)! $isunknown(multdiv_en)
ibex_multdiv_fast.IbexMultStateKnown	assert	States must be knwon/valid. disable iff((!rst_ni)!=='0)! $isunknown(mult_state_q)
ibex_multdiv_fast.IbexMultStateKnown	assert	States must be knwon/valid. disable iff((!rst_ni)!=='0)! $isunknown(mult_state_q)
ibex_multdiv_fast.IbexMultDivStateValid	assert	States must be knwon/valid. disable iff((!rst_ni)!=='0)(md_state_q inside {MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH})
ibex_fetch_fifo.IbexFetchFifoPushPopFull	assert	Must not push and pop simultaneously when FIFO full. disable iff((!rst_ni)!=='0)((in_valid_i && pop_fifo) |-> (! valid_q[DEPTH - 1] || clear_i))
ibex_fetch_fifo.IbexFetchFifoPushFull	assert	Must not push to FIFO when full. disable iff((!rst_ni)!=='0)(in_valid_i |-> (! valid_q[DEPTH - 1] || clear_i))
ibex_core.NoMemRFWriteWithoutPendingLoad	assert	When writing back the result of a load, the load must have made it to writeback disable iff((!rst_ni)!=='0)(rf_we_lsu |-> outstanding_load_wb)
ibex_core.NoMemRFWriteWithoutPendingLoad	assert	disable iff((!rst_ni)!=='0)(rf_we_lsu |-> outstanding_load_id)
ibex_core.NoMemResponseWithoutPendingAccess	assert	disable iff((!rst_ni)!=='0)(data_rvalid_i |-> (outstanding_load_resp | outstanding_store_resp))
ibex_core.NoExecWhenFetchEnableNotOn	assert	When fetch is disabled, no instructions should be executed. Once fetch is disabled either the ID/EX stage is not valid or the PC of the ID/EX stage must remain as it was at disable. The ID/EX valid should not ressert once it has been cleared. disable iff((!rst_ni)!=='0)(! fetch_enable_raw |=> ((~ instr_valid_id || (pc_id == pc_at_fetch_disable)) && ~ $rose(instr_valid_id)))
ibex_core.IbexCsrOpValid	assert	These assertions are in top-level as instr_valid_id required as the enable term disable iff((!rst_ni)!=='0)(instr_valid_id |-> (csr_op inside {CSR_OP_READ, CSR_OP_WRITE, CSR_OP_SET, CSR_OP_CLEAR}))
ibex_core.IbexCsrWdataIntKnownKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(csr_op_en)
ibex_core.IbexCsrWdataIntKnown	assert	disable iff((!rst_ni)!=='0)(csr_op_en |-> ! $isunknown(cs_registers_i.csr_wdata_int))
ibex_core.MultDivFSMIdleOnIdReady	assert	If the ID stage signals its ready the mult/div FSMs must be idle in the following cycle disable iff((!rst_ni)!=='0)(id_in_ready |=> ex_block_i.sva_multdiv_fsm_idle)
ibex_top.ScrambleKeyAppliedAtTagBank_A	assert	Ensure that when a scramble key is received, it is correctly applied to the icache scrambled memory primitives. The upper bound in the cycle ranges below is not exact, but it should not take more than 10 cycles. disable iff((!rst_ni)!=='0)(scramble_key_valid_i |-> (## [0 : 10] (tag_bank.key_valid_i && (tag_bank.key_i == sampled_scramble_key))))
ibex_top.ScrambleKeyAppliedAtDataBank_A	assert	disable iff((!rst_ni)!=='0)(scramble_key_valid_i |-> (## [0 : 10] (data_bank.key_valid_i && (data_bank.key_i == sampled_scramble_key))))
ibex_top.IbexInstrReqX	assert	X checks for top-level outputs disable iff((!rst_ni)!=='0)! $isunknown(instr_req_o)
ibex_top.IbexInstrReqPayloadXKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(instr_req_o)
ibex_top.IbexInstrReqPayloadX	assert	disable iff((!rst_ni)!=='0)(instr_req_o |-> ! $isunknown(instr_addr_o))
ibex_top.IbexDataReqX	assert	disable iff((!rst_ni)!=='0)! $isunknown(data_req_o)
ibex_top.IbexDataReqPayloadXKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(data_req_o)
ibex_top.IbexDataReqPayloadX	assert	disable iff((!rst_ni)!=='0)(data_req_o |-> ! $isunknown({data_we_o, data_be_o, data_addr_o, data_wdata_o, data_wdata_intg_o}))
ibex_top.IbexScrambleReqX	assert	disable iff((!rst_ni)!=='0)! $isunknown(scramble_req_o)
ibex_top.IbexDoubleFaultSeenX	assert	disable iff((!rst_ni)!=='0)! $isunknown(double_fault_seen_o)
ibex_top.IbexAlertMinorX	assert	disable iff((!rst_ni)!=='0)! $isunknown(alert_minor_o)
ibex_top.IbexAlertMajorInternalX	assert	disable iff((!rst_ni)!=='0)! $isunknown(alert_major_internal_o)
ibex_top.IbexAlertMajorBusX	assert	disable iff((!rst_ni)!=='0)! $isunknown(alert_major_bus_o)
ibex_top.IbexCoreSleepX	assert	disable iff((!rst_ni)!=='0)! $isunknown(core_sleep_o)
ibex_top.IbexTestEnX	assert	X check for top-level inputs disable iff((!rst_ni)!=='0)! $isunknown(test_en_i)
ibex_top.IbexRamCfgX	assert	disable iff((!rst_ni)!=='0)! $isunknown(ram_cfg_i)
ibex_top.IbexHartIdX	assert	disable iff((!rst_ni)!=='0)! $isunknown(hart_id_i)
ibex_top.IbexBootAddrX	assert	disable iff((!rst_ni)!=='0)! $isunknown(boot_addr_i)
ibex_top.IbexInstrGntX	assert	disable iff((!rst_ni)!=='0)! $isunknown(instr_gnt_i)
ibex_top.IbexInstrRValidX	assert	disable iff((!rst_ni)!=='0)! $isunknown(instr_rvalid_i)
ibex_top.IbexInstrRPayloadXKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(instr_rvalid_i)
ibex_top.IbexInstrRPayloadX	assert	disable iff((!rst_ni)!=='0)(instr_rvalid_i |-> ! $isunknown({instr_rdata_i, instr_rdata_intg_i, instr_err_i}))
ibex_top.IbexDataGntX	assert	disable iff((!rst_ni)!=='0)! $isunknown(data_gnt_i)
ibex_top.IbexDataRValidX	assert	disable iff((!rst_ni)!=='0)! $isunknown(data_rvalid_i)
ibex_top.MaxOutstandingDSideAccessesCorrect	assert	We should never start a new data request if we've already got the maximum outstanding. We can start a new request in the same cycle an old one ends, in which case we'll see all pending accesses valid but one will be ending this cycle so the empty slot can be immediately used by the new request. disable iff((!rst_ni)!=='0)(data_req_o |-> (~ pending_dside_accesses_q[MaxOutstandingDSideAccesses - 1].valid | data_rvalid_i))
ibex_top.PendingAccessTrackingCorrect	assert	Should only see a request response if we're expecting one disable iff((!rst_ni)!=='0)(data_rvalid_i |-> pending_dside_accesses_q[0])
ibex_top.IbexDataRPayloadXKnownEnable	assert	For SecureIbex responses to both writes and reads must specify rdata and rdata_intg (for writes rdata is effectively ignored by rdata_intg still checked against rdata) disable iff((!rst_ni)!=='0)! $isunknown(data_rvalid_i)
ibex_top.IbexDataRPayloadX	assert	disable iff((!rst_ni)!=='0)(data_rvalid_i |-> ! $isunknown({data_rdata_i, data_rdata_intg_i}))
ibex_top.IbexDataRPayloadXKnownEnable	assert	Without SecureIbex data_rdata_i and data_rdata_intg_i are only relevant to reads. Check neither are X on a response to a read. disable iff((!rst_ni)!=='0)! $isunknown((data_rvalid_i & pending_dside_accesses_q[0].is_read))
ibex_top.IbexDataRPayloadX	assert	disable iff((!rst_ni)!=='0)((data_rvalid_i & pending_dside_accesses_q[0].is_read) |-> ! $isunknown({data_rdata_i, data_rdata_intg_i}))
ibex_top.IbexDataRErrPayloadXKnownEnable	assert	data_err_i relevant to both reads and writes. Check it isn't X on any response. disable iff((!rst_ni)!=='0)! $isunknown(data_rvalid_i)
ibex_top.IbexDataRErrPayloadX	assert	disable iff((!rst_ni)!=='0)(data_rvalid_i |-> ! $isunknown(data_err_i))
ibex_top.DoubleFaultSinglePulse	assert	We should only have a single assertion of double_fault_seen in the delay buffer disable iff((!rst_ni)!=='0)$onehot0(double_fault_seen_delay_buffer)
ibex_top.DoubleFaultPulseSeenOnDoubleFault	assert	If we predict a double_fault_seen_o we should see one in the delay buffer disable iff((!rst_ni)!=='0)(double_fault_seen_predicted |-> | double_fault_seen_delay_buffer)
ibex_top.DoubleFaultPulseOnlyOnDoubleFault	assert	If double_fault_seen_o is asserted we should see predict one occurring within a bounded time disable iff((!rst_ni)!=='0)(double_fault_seen_o |-> (## [0 : DoubleFaultSeenLatency] double_fault_seen_predicted))
ibex_top.IbexIrqX	assert	disable iff((!rst_ni)!=='0)! $isunknown({irq_software_i, irq_timer_i, irq_external_i, irq_fast_i, irq_nm_i})
ibex_top.IbexScrambleKeyValidX	assert	disable iff((!rst_ni)!=='0)! $isunknown(scramble_key_valid_i)
ibex_top.IbexScramblePayloadXKnownEnable	assert	disable iff((!rst_ni)!=='0)! $isunknown(scramble_key_valid_i)
ibex_top.IbexScramblePayloadX	assert	disable iff((!rst_ni)!=='0)(scramble_key_valid_i |-> ! $isunknown({scramble_key_i, scramble_nonce_i}))
ibex_top.IbexDebugReqX	assert	disable iff((!rst_ni)!=='0)! $isunknown(debug_req_i)
ibex_top.IbexFetchEnableX	assert	disable iff((!rst_ni)!=='0)! $isunknown(fetch_enable_i)
ibex_top.WaddrAZeroForDummyInstr	assert	Dummy instructions may only write to register 0, which is a special register when dummy instructions are enabled. disable iff((!rst_ni)!=='0)((dummy_instr_wb && rf_we_wb) |-> (rf_waddr_wb == '0))
ibex_top.CrashDumpCurrentPCConn	assert	Ensure the crash dump is connected to the correct internal signals disable iff((!rst_ni)!=='0)(crash_dump_o.current_pc === u_ibex_core.pc_id)
ibex_top.CrashDumpNextPCConn	assert	disable iff((!rst_ni)!=='0)(crash_dump_o.next_pc === u_ibex_core.pc_if)
ibex_top.CrashDumpLastDataAddrConn	assert	disable iff((!rst_ni)!=='0)(crash_dump_o.last_data_addr === u_ibex_core.load_store_unit_i.addr_last_q)
ibex_top.CrashDumpExceptionPCConn	assert	disable iff((!rst_ni)!=='0)(crash_dump_o.exception_pc === u_ibex_core.cs_registers_i.mepc_q)
ibex_top.CrashDumpExceptionAddrConn	assert	disable iff((!rst_ni)!=='0)(crash_dump_o.exception_addr === u_ibex_core.cs_registers_i.mtval_q)
ibex_top.MajorAlertOnDMemIntegrityErr	assert	disable iff((!rst_ni)!=='0)((data_rvalid_i && | data_ecc_err) |-> (## [0 : 5] alert_major_bus_o))
ibex_top.MajorAlertOnIMemIntegrityErr	assert	Check alerts from memory integrity failures disable iff((!rst_ni)!=='0)((instr_rvalid_i && | instr_ecc_err) |-> (## [0 : 5] alert_major_bus_o))
push_pull_if.ReadyIsKnown_AKnownEnable	assert	The ready and valid signals should always have known values. disable iff((!rst_n)!=='0)! $isunknown(is_push_agent)
push_pull_if.ReadyIsKnown_A	assert	disable iff((!rst_n)!=='0)(is_push_agent |-> ! $isunknown(ready))
push_pull_if.ValidIsKnown_AKnownEnable	assert	disable iff((!rst_n)!=='0)! $isunknown(is_push_agent)
push_pull_if.ValidIsKnown_A	assert	disable iff((!rst_n)!=='0)(is_push_agent |-> ! $isunknown(valid))
push_pull_if.H_DataKnownWhenValid_AKnownEnable	assert	Whenever valid is asserted, h_data must have a known value. disable iff((!rst_n)!=='0)! $isunknown((valid && is_push_agent))
push_pull_if.H_DataKnownWhenValid_A	assert	disable iff((!rst_n)!=='0)((valid && is_push_agent) |-> ! $isunknown(h_data))
push_pull_if.D_DataKnownWhenReady_AKnownEnable	assert	Whenver ready is asserted and the agent is in bidirectional mode, d_data must have a known value. disable iff((!rst_n)!=='0)! $isunknown(((ready && is_push_agent) && in_bidirectional_mode))
push_pull_if.D_DataKnownWhenReady_A	assert	disable iff((!rst_n)!=='0)(((ready && is_push_agent) && in_bidirectional_mode) |-> ! $isunknown(d_data))
push_pull_if.H_DataStableWhenValidAndNotReady_A	assert	When valid is asserted but ready is low the h_data must stay stable. disable iff((!rst_n)!=='0)(is_push_agent |-> ((valid && ! ready) |=> $stable(h_data)))
push_pull_if.ValidHighUntilReady_A	assert	When valid is asserted, it must stay high until seeing ready be asserted. disable iff((!rst_n)!=='0)(is_push_agent |-> ($rose(valid) |-> (valid throughout (ready [-> 1]))))
push_pull_if.ReqIsKnown_AKnownEnable	assert	The req and ack signals should always have known values. disable iff((!rst_n)!=='0)! $isunknown(! is_push_agent)
push_pull_if.ReqIsKnown_A	assert	disable iff((!rst_n)!=='0)(! is_push_agent |-> ! $isunknown(req))
push_pull_if.AckIsKnown_AKnownEnable	assert	disable iff((!rst_n)!=='0)! $isunknown(! is_push_agent)
push_pull_if.AckIsKnown_A	assert	disable iff((!rst_n)!=='0)(! is_push_agent |-> ! $isunknown(ack))
push_pull_if.D_DataKnownWhenAck_AKnownEnable	assert	When ack is asserted, d_data must have a known value. disable iff((!rst_n)!=='0)! $isunknown((ack && ! is_push_agent))
push_pull_if.D_DataKnownWhenAck_A	assert	disable iff((!rst_n)!=='0)((ack && ! is_push_agent) |-> ! $isunknown(d_data))
push_pull_if.H_DataKnownWhenReq_AKnownEnable	assert	When req is asserted and the agent is in bidirectional mode, h_data must have a known value. disable iff((!rst_n)!=='0)! $isunknown(((req && ! is_push_agent) && in_bidirectional_mode))
push_pull_if.H_DataKnownWhenReq_A	assert	disable iff((!rst_n)!=='0)(((req && ! is_push_agent) && in_bidirectional_mode) |-> ! $isunknown(h_data))
push_pull_if.H_DataStableWhenBidirectionalAndReq_A	assert	When req is asserted but ack is low, and the agent is in bidirectional mode, h_data must remain stable. disable iff((!rst_n)!=='0)((! is_push_agent && in_bidirectional_mode) |-> ((req && ! ack) |=> $stable(h_data)))
push_pull_if.AckAssertedOnlyWhenReqAsserted_A	assert	I 2-phase req-ack handshake, ack cannot be 1 if req is not 1. disable iff((!rst_n)!=='0)((! is_push_agent && ! is_pull_handshake_4_phase) |-> (ack |-> req))
push_pull_if.NoAckOnNewReq_A	assert	Req is asserted only after previous ack is de-asserted. disable iff((!rst_n)!=='0)(! is_push_agent |-> ($rose(req) |-> (! $past(ack, 1) && ! ack)))
push_pull_if.ReqHighUntilAck_A	assert	When req is asserted, it must stay high until a corresponding ack is seen. disable iff((!rst_n)!=='0)(! is_push_agent |-> ($rose(req) |-> (req throughout (ack [-> 1]))))
push_pull_if.AckHighUntilReq_A	assert	When ack is asserted, it must stay high until a corresponding req is de-asserted, in case of four-phase handshake. disable iff((!rst_n)!=='0)((! is_push_agent && is_pull_handshake_4_phase) |-> ($rose(ack) |-> (ack throughout (! req [-> 1]))))
core_ibex_fcov_if.InstrCategoryALUCorrect	assert	The ALU category is tricky as there's no specific ALU enable and instructions that actively use the result of the ALU but aren't themselves ALU operations (such as load/store and JALR). This categorizes anything that selects the ALU as the source of register write data and enables register writes minus some exclusions as an ALU operation. disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryALU) |-> ((((((id_stage_i.rf_wdata_sel == RF_WD_EX) && id_stage_i.rf_we_dec) && ~ id_stage_i.mult_sel_ex_o) && ~ id_stage_i.div_sel_ex_o) && ~ id_stage_i.lsu_req_dec) && ~ id_stage_i.jump_in_dec))
core_ibex_fcov_if.InstrCategoryMulCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryMul) |-> id_stage_i.mult_sel_ex_o)
core_ibex_fcov_if.InstrCategoryDivCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryDiv) |-> id_stage_i.div_sel_ex_o)
core_ibex_fcov_if.InstrCategoryBranchCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryBranch) |-> id_stage_i.branch_in_dec)
core_ibex_fcov_if.InstrCategoryJumpCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryJump) |-> id_stage_i.jump_in_dec)
core_ibex_fcov_if.InstrCategoryLoadCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryLoad) |-> (id_stage_i.lsu_req_dec && ! id_stage_i.lsu_we))
core_ibex_fcov_if.InstrCategoryStoreCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryStore) |-> (id_stage_i.lsu_req_dec && id_stage_i.lsu_we))
core_ibex_fcov_if.InstrCategoryCSRAccessCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryCSRAccess) |-> id_stage_i.csr_access_o)
core_ibex_fcov_if.InstrCategoryEBreakDbgCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryEBreakDbg) |-> (id_stage_i.ebrk_insn && id_stage_i.controller_i.ebreak_into_debug))
core_ibex_fcov_if.InstrCategoryEBreakExcCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryEBreakExc) |-> (id_stage_i.ebrk_insn && ! id_stage_i.controller_i.ebreak_into_debug))
core_ibex_fcov_if.InstrCategoryECallCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryECall) |-> id_stage_i.ecall_insn_dec)
core_ibex_fcov_if.InstrCategoryMRetCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryMRet) |-> id_stage_i.mret_insn_dec)
core_ibex_fcov_if.InstrCategoryDRetCorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryDRet) |-> id_stage_i.dret_insn_dec)
core_ibex_fcov_if.InstrCategoryWFICorrect	assert	disable iff((!rst_ni)!=='0)((id_instr_category == InstrCategoryWFI) |-> id_stage_i.wfi_insn_dec)
core_ibex_fcov_if.InstrCategoryFenceICorrect	assert	disable iff((!rst_ni)!=='0)(((id_instr_category == InstrCategoryFenceI) && id_stage_i.instr_first_cycle) |-> id_stage_i.icache_inval_o)
core_ibex_tb_top.NoAlertsTriggered	assert	We should never see any alerts triggered in normal testing disable iff((!rst_n)!=='0)((! dut_if.alert_minor && ! dut_if.alert_major_internal) && ! dut_if.alert_major_bus)