Skip to content

Commit bbca017

Browse files
committed
[rtl] Add assertion to ensure the push/pop FSM only advances if valid
1 parent 9f2c7c0 commit bbca017

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

rtl/ibex_compressed_decoder.sv

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -806,5 +806,6 @@ module ibex_compressed_decoder #(
806806
!$isunknown({instr_i[12], instr_i[6:5]}))
807807
`ASSERT(IbexC2Known1, (valid_i && (instr_i[1:0] == 2'b10)) |->
808808
!$isunknown(instr_i[15:13]))
809+
`ASSERT(IbexPushPopFSMStable, !valid_i |-> cm_state_d == cm_state_q)
809810

810811
endmodule

0 commit comments

Comments
 (0)