As mentioned in a source code TODO, properly doing model equivalence checking on the AsyncFIFO requires using Yosys' multiclock formal support. Currently we check that it meets the FIFOContractSpec in the specific case that read_clk and write_clk are exactly in phase, which is useful, but not complete.

Basically just wanted this to be tracked in the issues instead of in a TODO.