In stream_xbar module, when flush_i is asserted, ready_o[31] remains unset (not set to 0).

[mhayat-10xe]

I wrote this assertion and it is failing.

generate
    for (genvar inp = 0; inp < NumInp ; inp++ ) 
     
     assrt8_flush_with_ready_0: // when flush_i is asserted ready_o should be zero
     assert property(flush_i |-> ready_o[inp]==0);

  endgenerate

It passes for all other ready_o, but fails for ready_o[31].

[mhayat-10xe]

Hi @niwis,
is this a bug or there is a problem in my understanding?

[niwis]

Hi @hayat10x, according to the signal description, valid_i should be deasserted during flush_i. Is this the case in your counterexample?

common_cells/src/stream_xbar.sv

Lines 57 to 61 in 69d40a5

	/// Flush the state of the internal `rr_arb_tree` modules.
	/// If not used set to `0`.
	/// Flush should only be used if there are no active `valid_i`, otherwise it will
	/// not adhere to the AXI handshaking.
	input logic flush_i,

Also, note that flush_i only resets the internal state of the round-robin arbiter. If this is misleading, feel free to propose a different solution.

[mhayat-10xe]

yes, valid_i is deasserted in the case when flush_i is asserted.
I wrote the assumption for flush_i as follows:

assmp5_flush_i:  // flush should only be asserted if there is no active valid_i
assume property(flush_i |->  valid_i == 0 );

[niwis]

could you share a waveform? Also, to clarify, flush_i only resets the internal state of the round-robin arbiter, which determines which input is being served in the following cycles.

[mhayat-10xe]

So when the internal state of the arbiter is reset, won't it affect ready_o?
Here is the waveform where you can see that valid_i = 0, and all other ready_o indexes are flushed except ready_o[31].

[niwis]

@hayat10x we would need more visibility to debug this. could you share a reproducible testbench or a data format containing all internal signals?
Adding @thommythomaso to the discussion

[mhayat-10xe]

Hi @niwis, I apologize for the delayed response. Unfortunately, access to the JasperGold license has been discontinued. I will provide all the internal signals once it becomes available again. Thanks