amaranth
amaranth copied to clipboard
amaranth-lang
r_data is undefined after a simultaneous write to an empty AsyncFIFO
The behavior of a dual port block RAM with read and write ports in different clock domains is not defined during a simultaneous read and write to the same address. (In fact it is not possible to make it defined.) However, this is exactly what is happening when an element is written into an empty AsyncFIFO[Buffered], since the produce and consume pointers are equal. If the phase of read and write clocks is just wrong, the output register of the BRAM could end in a metastable state.
It is not clear how this can be fixed. A workaround is to use AsyncFIFOBuffered instead, which resynchronizes the BRAM output.
I think what Xilinx does here is they require you to add a pipeline register in the dual-clock FIFO, effectively constructing a 2FF synchronizer out of the BRAM output register and the pipeline register.
Which seems fine semantically, but... does this mean that bare AsyncFIFO should never be used?
To fix this problem, we can add a small amount of logic that prevents this kind of condition from arising. We can convince ourselves that it's sound using formal verification.
