Ben Cohen
Write assertion for signal “B” will be low after the start bit becomes high within the range of [4:15] clock cycles. “B” will be high at posedge of “A” till this time “B” should be low. See the below diagram for reference.
In reply to Mrutunjay:
clocking df_clk @(posedge clk);
endclocking
default clocking df_clk;
property p1;
$rose(start)|-> ##[4:15] $fell(B) ##0 !B[*1:$] ##1 $rose(A) ##0 B;
endproperty
assert property (p1);
- I guess this will satiate your requirement. I am unsure whether I should use first_match over here cause I am assuming the tool will automatically defenestrate other possible scenarios.
In reply to Shubhabrata:
Hi Shubhabrata,
Thank you for the solution.
while i was trying this assertion “A” is high @ same clock edge if “B” is high then assertion passed. But, when I tried passing “B” before “A” the assertion was checking upto 15 clock cycles and it failed at 15th clock cycle. But, we need assertion to fail when “B” is high (at that clock-edge only) it should not check for all 15 clock cycles.
In reply to Mrutunjay:
Ok, I think I got it. You are prioritizing signal B. So simply put signal B before $rose(A) inside that assertion. I believe it’ll work.
clocking df_clk @(posedge clk);
endclocking
default clocking df_clk;
property p1;
$rose(start)|-> ##[4:15] $fell(B) ##0 !B[*1:$] ##1 B ##0 $rose(A);
endproperty
assert property (p1);
Now If you are focusing on the first appearance of $fell(B) in that range, then you can think of using the first_match() construct.
In reply to Shubhabrata:
The problem I am getting is
assertion should check “B” is low till “A” is high and then “B” should become high at same clock edge of “A”.
from your solution if I try to make “B” high before “A”. The assertion is still passing when both “A” and “B” are high after.
In the below diagram assertion should fail at 85 only but it passing at 125 because “A” and “B”
both are High.
In reply to Mrutunjay:
Hi,
There are a few confusions you have I believe regarding the sampling of signals in the assertion. Sampled values of both “A” and “B” are 1 at 165, not at 125. And yes It should have given an error when “B” has been sampled as 1 before “A” got sampled as 1. But this scenario has been observed at 95, not at 85.
Now if you observe the waveform, you will see that $fell(B) is happening (w.r.t $rose(start)) two times - at 75 and at 105.
The unwanted result/success you are getting is happening due to $fell(B) that’s observed at 105. As it falls inside that [4:15] range.
I reckon the tool is getting all the threads and completing the assertion w.r.t each and every one of them. Honestly speaking I don’t know why this is happening.
I believe the usage of the first_match() construct will suffice this matter.
clocking df_clk @(posedge clk);
endclocking
default clocking df_clk;
property p1;
$rose(start)|-> first_match(##[4:15] $fell(B) ##0 !B[*1:$] ##1 B) ##0 $rose(A);
endproperty
assert property (p1);
Please let me know whether it’s working or not.