Skip to content

Multi-clock formal for AsyncFIFO test cases #387

Open
@awygle

Description

@awygle

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.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions