However, this doesn’t work with len==0. The situation of $rose(s1) ##0 $rose(s2) with len==0 is also valid. So, I’d like to include len==0 case to the property. Variable wait sequence in stead of variable s1 continuation like the following might be considered.
What is the intention in following case ::
After 1st assertion of s1 (0->1), s1 is de-asserted (1->0) at the same time as s2 is asserted (0->1) ?
Using the above code the assertion would pass due to ‘or’ at de-assertion of s1
Thank you for your proposal. But it looks the property you proposed is different from what I want to check. What I want to check is “whether the clock cycle number between rising edges of two signals is same as the specified value.”
No, s1 is kept high when s2 is asserted(0->1). But this s1 behavior is not quite related to this matter. The point is how to count cycle number before s2 assert(0->1).
If you insist on using a counter approach I would suggest a few changes to your code
Using !s1 ##1 $rose(s1) , is it necessary for s1 to be low in the start ?
What if you simply used $rose(s1) instead ?
Any particular reason you have used non-overlapping implication operator |=> ?
When the antecedent has a match, you could check the consequent at the same clock using |->
The reason why I used 1. !s1 ##1 $rose(s1) and 2 . |=> is similar. I just wanted
to separate internal counter increment cycle from counter initialization cycle and check cycle. By 1, I wanted to clarify counter initialization and counter increment are done in a different cycle. By 2, the check is done after the last counter increment cycle. They are only for safety just in case. A property without them would properly work as you have attempted in EDA Playground.
There is a large number of experts who abhor the use of the first_match
because of efficiency; also, it is not used in PSL.
Below is another option without the first_match.
I like the v_cnt += !s2
I will replace first_match with intersect s2[->1].
But note that a certain license free simulator doesn’t properly work with intersect s2[->1] while first_match usage is O.K . It is simulator’s issue, though.
It means “v_cnt is incremented while s1 is 1 except s2 is 1”.
I wanted to check the distance between s1 rise and s2 rise. So, the condition of s1 == 1 is necessary. Otherwise, the following distance would also be checked with (1, v_cnt += !s2)