Need help understanding formal verification of asynchronous FIFO

[Anand]

Hi everyone,

I’m new to formal verification and trying to learn how to apply it to an asynchronous FIFO design (different write and read clocks).
I don’t have much experience with this topic, so I’m not sure how to start what properties to write, how to set up the environment, or how to check correctness formally.

[ysgyryd]

@Anand

and trying to learn how to apply it to an asynchronous FIFO design (different write and read clocks).
I don’t have much experience with this topic, so I’m not sure how to start what properties to write, how to set up the environment, o

This ZipCPU blog might be a good place to start with the topic: Crossing clock domains with an Asynchronous FIFO

It doesn’t talk about setting up an environment directly in that blog post but gives a good overview of the formal properties used