Need clarification of assertions failure in stream_xbar module

[mhayat-10xe]

assrt2_stable_idx_o: // idx_o remains stable when there is no ready_i and valid_o is high assert property (valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]));

assrt3_stable_data_o: // data_o remains stable when there is no ready_i and valid_o is high
assert property (valid_o[i] && !ready_i[i] |=> $stable(data_o[i]));

These two assertions fail when OutSpillReg is set to 0. Shouldn't it be stable?

[niwis]

Are the inputs (specifically valid_i, idx_i, data_i) stable?

[mhayat-10xe]

Yes, the inputs are stable. I wrote the assumption for inputs as follows:

generate for (genvar i = 0; i < NumInp; i++) begin

assmp1_stable_inputs: // valid_i, data_i and sel_i remains stable when ready_o is low and valid_i is high. assume property (valid_i[i] && !ready_o[i] |=> $stable(data_i[i]) && $stable(sel_i[i]) && valid[i]);

end

[niwis]

Then, I would agree that the outputs should be stable. Do you have a trace for a counter example?

[mhayat-10xe]

Yes, I have attached the trace. Here idx_o should remain stable in the second cycle.

[mhayat-10xe]

also can you please tell me the condition of ready_o to be high(specifically after how many cycles when some event occurs?)

[niwis]

could you email me the entire wlf (or any other format) of the trace including all signals? nwistoff@iis.ee.ethz.ch

also can you please tell me the condition of ready_o to be high(specifically after how many cycles when some event occurs?)

I don't have these numbers. But it should be possible to find this out by analyzing the source code (or RTL simulation)

[mhayat-10xe]

Sorry, there was an issue from my side. I forgot to write an assumption for flush_i that's why it was showing this behavior. Now these assertions are passing by writing constraint on fllush_i.