Hi:Originally posted in cdnusers.org by binju
In PSL/SVA, there is a type of assertions called liveness assertion. Liveness assertion is very good to check fairness and starvation. Let me give a simple example. If you want to check for a round robin arbiter starvation, you can capture the assertion in English as "if channel A gets a request, it eventually needs to be granted". Then you can write assertion like:
// psl reqA |-> eventually gntA;
In SVA, reqA |-> ##[0:$] gntA;
Does this make sense to you?