Following start after 0 to 3 cycles valid is asserted
and remains active (1) for 10 cycles and de-asserted for 20 cycles
(this pattern repeats when start is asserted and until finish is assert/
(start==1 then 0, … valid==1 for 10 cycles the 0 for 20 cycles…) repeats until the_finish
initial // Only one occurrence of the assertion
begin
ap: assert property(@ (posedge clk) $rose(start)[->1] |->
($rose(start) ##[1:3]valid[*10] ##1 !valid[*20])[*1:$])[*1:$] s_until thefinish);
// Also OK
ap: assert property(@ (posedge clk) $rose(start)[->1] |->
strong( ($rose(start) ##[1:3]valid[*10] ##1 !valid[*20])[*1:$])[*1:$] intersect
thefinish[->1]));
end
Thanks for the reply. The first valid signal will be asserted when start is asserted. Between start and finish there will be multiple times valid (10 cycles on/20 cycles off) will occur.
Why are there (2) [*1:$] at the end of the first property ?
The first valid signal will be asserted when start is asserted. Between start and finish there will be multiple times valid (10 cycles on/20 cycles off) will occur.
use ##[0:3] (see below)
Why are there (2) [*1:$] at the end of the first property ?
typo, sorry!
initial // Only one occurrence of the assertion
begin
ap: assert property(@ (posedge clk) $rose(start)[->1] |->
($rose(start) ##[0:3]valid[*10] ##1 !valid[*20])[*1:$] s_until thefinish);
// Also OK
ap: assert property(@ (posedge clk) $rose(start)[->1] |->
strong( ($rose(start) ##[0:3]valid[*10] ##1 !valid[*20])[*1:$]) intersect
thefinish[->1]));
end