I recently took an opportunity to review mkFabric_AXI4.v using a formal AXI4 property checker under SymbiYosys. It appears to have some difficulties routing packets from the correct source to the correct destination. The attached (abbreviated) trace should give you an idea of what I'm talking about.
In this example, a burst packet presented from master 0 gets routed to slave 0. The associated W* channel data, however, gets corrupted in the process. (The appropriate WSTRB value sent by the master was 0, not 4.) Not shown are two similar bursts presented from master 1 during this time which may (or may not be) relevant.
Hello, Dan, just acknowledging your report to assure you it hasn't fallen through the cracks; I will study it as soon as I can (currently swamped on another project). Rgds.
I recently took an opportunity to review mkFabric_AXI4.v using a formal AXI4 property checker under SymbiYosys. It appears to have some difficulties routing packets from the correct source to the correct destination. The attached (abbreviated) trace should give you an idea of what I'm talking about.
In this example, a burst packet presented from master 0 gets routed to slave 0. The associated W* channel data, however, gets corrupted in the process. (The appropriate WSTRB value sent by the master was 0, not 4.) Not shown are two similar bursts presented from master 1 during this time which may (or may not be) relevant.
Dan