[cov] Remove pointless cross

This cross wasn't much use as many of the transitions it was crossing
with instruction types only occur when the pipeline is empty (so there's
no instruction type to check).

The remaining interesting cases are already covered by other crosses
(e.g. `debug_if_entry_instr_cross` and `pipe_flush_instr_cross`).

Also adds an assertion to check the pipe is empty when we transition to
IRQ_TAKEN (we need this condition to hold to ensure we don't need extra
coverage for instruction types on this transition).
This commit is contained in:
Greg Chadwick 2022-10-27 14:31:47 +01:00 committed by Greg Chadwick
parent 2f9fd69ec4
commit bb92ea6df4
3 changed files with 8 additions and 35 deletions

View file

@ -177,23 +177,22 @@ Each pipeline stage has some associated state.
* Controller (within ID stage) state machine states
* ``cp_controller_fsm`` - Possible transitions between these states.
Those marked with a '*' are of particular interest and should be crossed with instruction categories and other coverpoints as appropriate to fully explore the transitions.
* ``RESET`` -> ``BOOT_SET``
* ``BOOT_SET`` -> ``FIRST_FETCH``
* ``FIRST_FETCH`` -> ``DECODE``
* ``FIRST_FETCH`` -> ``IRQ_TAKEN``
* ``FIRST_FETCH`` -> ``DBG_TAKEN_IF``
* ``DECODE`` -> ``FLUSH`` *
* ``DECODE`` -> ``DBG_TAKEN_IF`` *
* ``DECODE`` -> ``IRQ_TAKEN`` *
* ``DECODE`` -> ``FLUSH``
* ``DECODE`` -> ``DBG_TAKEN_IF``
* ``DECODE`` -> ``IRQ_TAKEN``
* ``IRQ_TAKEN`` -> ``DECODE``
* ``DBG_TAKEN_IF`` -> ``DECODE``
* ``DBG_TAKEN_ID`` -> ``DECODE``
* ``FLUSH`` -> ``DECODE`` *
* ``FLUSH`` -> ``DECODE``
* ``FLUSH`` -> ``DBG_TAKEN_ID``
* ``FLUSH`` -> ``WAIT_SLEEP``
* ``FLUSH`` -> ``DBG_TAKEN_IF`` *
* ``FLUSH`` -> ``DBG_TAKEN_IF``
* ``WAIT_SLEEP`` -> ``SLEEP``
* ``SLEEP`` -> ``FIRST_FETCH``

View file

@ -578,35 +578,6 @@ interface core_ibex_fcov_if import ibex_pkg::*; (
misaligned_insn_bus_err_cross: cross id_stage_i.instr_fetch_err_i,
id_stage_i.instr_fetch_err_plus2_i;
controller_instr_cross: cross cp_controller_fsm, cp_id_instr_category {
// Only expecting DECODE => FLUSH when we have the instruction categories constrained below.
bins decode_to_flush =
binsof(cp_controller_fsm.out_of_decode0) &&
binsof(cp_id_instr_category) intersect {InstrCategoryMRet, InstrCategoryDRet,
InstrCategoryEBreakDbg, InstrCategoryEBreakExc,
InstrCategoryECall, InstrCategoryFetchError,
InstrCategoryCSRAccess,
InstrCategoryCSRIllegal,
InstrCategoryUncompressedIllegal,
InstrCategoryCompressedIllegal,
InstrCategoryPrivIllegal,
InstrCategoryOtherIllegal};
bins decode_to_dbg = binsof(cp_controller_fsm.out_of_decode1);
bins decode_to_irq = binsof(cp_controller_fsm.out_of_decode2);
// Only expecting FLUSH => DECODE when we have the instruction categories constrained below.
bins flush_to_decode =
binsof(cp_controller_fsm.out_of_flush0) &&
!binsof(cp_id_instr_category) intersect {InstrCategoryEBreakDbg, InstrCategoryWFI};
// Only expecting FLUSH => IRQ_TAKEN when we have InstrCategoryCSRAccess in ID/EX
bins flush_to_irq_taken =
binsof(cp_controller_fsm.out_of_flush3) &&
binsof(cp_id_instr_category) intersect {InstrCategoryCSRAccess};
// Only expecting FLUSH => DEBUG_IF when we have InstrCategoryEBreakDbg in ID/EX
bins flush_to_dbg_if =
binsof(cp_controller_fsm.out_of_flush4) &&
!binsof(cp_id_instr_category) intersect {InstrCategoryEBreakDbg};
}
// Include both mstatus.mie enabled/disabled because it should not affect wakeup condition
irq_wfi_cross: cross cp_controller_fsm_sleep, cs_registers_i.mstatus_q.mie iff
(id_stage_i.irq_pending_i | id_stage_i.irq_nm_i);

View file

@ -895,6 +895,9 @@ module ibex_controller #(
end
end
`ASSERT(PipeEmptyOnIrq, ctrl_fsm_cs != IRQ_TAKEN & ctrl_fsm_ns == IRQ_TAKEN |->
~instr_valid_i & ready_wb_i);
//////////
// FCOV //
//////////