could you please clarify how to write assertion for the following
if a is asserted b should be asserted and the following sequence should be repeated as long as a is asserted.
b should be asserted for one clock cycle and then b should be deasserted for 32 clock cycles . the under
lined sequence should be repeated as long as a is asserted
Text
Text
assert property( @(posedge clk) a|→ ((b##1 !b[*32])[*1:$]intersect a[*1:$] )[*0: $] ##1 !a
would the above one correct?
Assume that clocking events i.e posedge of clk occurs at T0,T1,T2,T3…..Tn. ‘a’ is asserted at 2nd clocking event i.e T1. So ‘b’ should be asserted at T1 as well ( I assume ‘b’ could be high prior to assertion of ‘a’ as well ). ‘b’ should be sampled low for next 32 clocks i.e from T2 to T33.
Indirectly ‘a’ should be asserted from T1 to T33 i.e 33 clocks
A few questions
(Q1) If ‘a’ is sampled low at any clock from T2 to T33 then should the assertion should fail at the respective clock ?
(Q2) If ‘a’ is sampled low at T34 then should the assertion pass ? If yes, what should the sampled value of ‘b’ be at T34 ?
(Q3) If ‘a’ is sampled high at T:34 then should ‘b’ be high ? i.e 2nd iteration of b ##1 !b[*32]
If yes, when should ‘a’ be sampled low next and what should the value of ‘b’ be at that clock ?
Q1 . not required.
Q2.Yes assertion should pass. b can be anything.
a is asserted high for complete iteration
So essentially as long as ‘a’ is sampled high, ‘b’ should follow the sequence
If ‘a’ goes low at the next clock of being asserted, the assertion should pass irrespective of the value of ‘b’
I believe the following should work ( not tested but looks promising )
property a_b_seq;
$rose(a) |=> (( b ##1 !b[*0:32] )[*0:$] ##1 1 ) intersect $fell(a)[->1];
endproperty
assert property( @(posedge clk) a_b_seq );