Stucked at UART formal verification

it has been decades since i designed a UART; however, if I recall it well, there is a 16x clock at the receiver. Thus, when you say “I am now planning for asynchronous clocks testing where the Tx and Rx clocks would be [b]slightly different in frequency and phase” I don’t really understand it. Typically, the tx 16x clock and rx 16x clock are of the same frequency, but not the same phase. Those frequencies can vary a bit and the 16x rate allows for some s=deviations between the rx and tx clock. Is this what you mean?

How am I going to assert() when I have two different clocks ?

You could simply have 2 counters, one for the tx and one for rx.
Let those clocks count for 100 or 1000 cycles, and then compare the values of the counts. From there you can assess the frequency differences. SVA would not do too well on this.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf