amaranth icon indicating copy to clipboard operation
amaranth copied to clipboard

Multi-clock formal for AsyncFIFO test cases

Open awygle opened this issue 4 years ago • 0 comments

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.

awygle avatar May 16 '20 23:05 awygle