To check that a signal toggles at least once every 20 cycles

property ppt;
@(posedge clk) (sig_a ==0 || sig_a ==1 ) |-> ##[1:20]$changed(sig_a);
endproperty

            assert_property:assert property(ppt);

I tried doing this way. Can someone help me out this.
Thanks,
Gyaneshwar

module tb;
  bit clk;
  bit sig_a;

  always #1 clk = ~clk;
  property ppt;
    @(posedge clk) (sig_a==0 || sig_a==1)
      ##[0:20] $changed(sig_a);
  endproperty

  assert_property: assert property(ppt)
    $display("Assertion passed at time=%0t", $time);
  else
    $display("Assertion failed at time=%0t", $time);

  initial begin
    sig_a = 1;
    #6 sig_a = 0;    
    #20 sig_a = 1;   
    #14 sig_a = 0;     
    #60 $finish;    
  end

  initial begin
    $dumpfile("dump.vcd");
    $dumpvars;
  end
endmodule

The correct property is

property ppt;
    @(posedge clk) $changed(sig_a) |->
      ##[1:20] $changed(sig_a);
endproperty

And you probably need one other assertion that it toggles once in the first 20 cycles.

Hi Dave,
Would like to hear your thoughts on the following
Using always #5 clk = !clk;
For the 1st attempt starting at T:5, sig_a must change before it’s 20th posedge at time: 205 units
For the 2nd attempt starting at T:15, sig_a must change before it’s 20th posedge at time: 215 units
For the 3rd attempt starting at T:25, sig_a must change before it’s 20th posedge at time: 225 units etc.

module top_tb;
   bit   clk; 
  logic  sig_a ;
 
  always #5 clk = !clk;
  
  property ppt;
    @(posedge clk) ##[1:20]$changed(sig_a);
  endproperty
  
  assert property( ppt ) $display("T:%0t Pass",$time); 
                    else $display("T:%0t Fails",$time);    
    
  initial #260 $finish();
endmodule

I observe output( for the 6 attempts from time:5 to time:55 ) as
T:205 Fails
T:215 Fails
T:225 Fails
T:235 Fails
T:245 Fails
T:255 Fails

The interesting thing that I note is that even though ‘sig_a’ remains at default value of ‘X’ , $changed detects the no-change

Does this mean that all the Sampled value functions ( $rose/$fell/$past/$stable/$changed/$sampled ) use ‘===’ and not ‘==’ internally ?

1 Like

In what cases will the below fail?

property sig_tog;
  @(posedge clk)
  $fell(a) |-> ##[1:20] $rose(a); 
endproperty

NVM, Got it

@whizclips
So how would sig_tog flag an error if ‘a’ were to remain at default value ( similar to Arshi’s case ) throughout simulation ?

Hi Gyan21,
There are 2 ways that one could interpret the intention

Suppose the clocking event occurs at T0 ( first clocking event) ,T1 ( second clocking event) , …Tn ( (n+1)th clocking event)

(1) There is 1 attempt every 20 clocks
For the 1st attempt which starts at T0, sig_a must toggle within the next 20 clocks ( T1 to T20 )
The 2nd attempt would start at T21, sig_a must toggle within the next 20 clocks ( T22 to T41 )
The 3rd attempt would be start at T42, sig_a must toggle within the next 20 clocks ( T43 to T62 )

(2) There is an attempt at each clock
So if the first change in sig_a were to occur at 21st clocking event i.e T20
Each of the initial 20 attempts from T0 to T19 would result in execution of pass action block at T20

Which one amongst the above two fits your intention ?

Hi @LFT,

There is 1 attempt every 20 clocks
you can interpret it in this way.