I am currently working on the formal verification of the stream_xbar. During my analysis, I have identified an abnormality in its behavior.
In the 2nd clock cycle of the picture below, we have requests for output number 4 simultaneously. However, in the 3rd clock cycle, idx_o[4] serves input number 3, which is incorrect. It should serve input number 2 first, and then input number 3 should be served afterward. Is this a bug or a lack of understanding from my side?
