How to write assertion that checks the signal till the end of simulation

SystemVerilog
1

Hi,

I want to write assertion for:
Once enable goes high in the next cycle, one pulse on signal “a” (whose width is equal to one clock cycle) should be generated and from there it should be generated for every ten clock cycles.
Can anyone help me with the assertion. How to check signal “a” till the end of simulation?

Thanks

2

In reply to curious_verifier:
Once enable goes high // $rose(enable)
in the next cycle, // ##1
one pulse on signal “a” (whose width is equal to one clock cycle)// a
should be generated and from there // always
it should be generated for every ten clock cycles. // a ##1 !a[*9]


initial // needed to ensure ONE attempt
// the goto [->1] is needed because we don't know when the rose of enable will occur
// the always ensure that the sequence ##1 a ##1 ![*9] is repeated forever
  ap_enb_aevery10: assert property(@(posedge clk) $rose(enable)[->1] |-> 
                             s_always (##1 a ##1 !a[*9]));  // ???
//[Ben] Serious Doubt about the above 
// because (##1 a ##1 !a[*9] is not true at every clock tick, 
/* 1800: Thus, it is more precise to say that s_always[n:m] property_expr evaluates to true if, and only if, there exist m+1 ticks of the clock of the always property, including the current time step, and property_expr evaluates to true beginning in all of the n+1 to m+1 clock ticks, where counting starts at the current time step. */

// Could also use: 
  initial 
   ap_enb_aevery10b: assert property(@(posedge clk) $rose(enable)[->1] |-> 
                             strong (##1 a ##1 !a[*9])[*2^31);

Also, you did not address the case if enable can fall again. This is an incomplete set f requirements for these 2 signals.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to curious_verifier:

Try few simple ones:



  // Once enable goes high in the next cycle, one pulse on signal "a" 
  $rose(enable) |=> $rose(a)
  // (whose width is equal to one clock cycle)
  $rose (a) |=> !a[*8]

  // should be generated for every ten clock cycles.
  $rose(a) |=> ##9 $rose(a)

  // May need small tweaks, untested

Good luck
Srini

4

Hi Ben,

Thanks for the reply. enable is high is only for one cycle at the start.

5

In reply to curious_verifier:
I would implement one of those options:


// Option 1 
initial begin 
  ap_enb: assert property(@(posedge clk) $rose(enable)[->1] |=> always(!enable));
  ap_enb_aevery10: assert property(@(posedge clk) $rose(enable)[->1] |-> 
                             strong (##1 $rose(a) ##1 !a[*9])[*2^31);
// Note: the s_always requires a range. If no range, use the s_eventually 
// 1800 syntax: 
// s_always [ constant_range] property_expr  
// s_eventually property_expr 
end

//option 2 $rose (a) |=> !a[*9] ##1 $rose(a);
initial  
  ap_enb: assert property(@(posedge clk) $rose(enable)[->1] |=> always(!enable) and $rose(a));
// Concurrent assertion
  ap_aevery10: assert property(@(posedge clk) $rose(a) |=> 
                          strong(!a[*9] ##1 $rose(a)));

A note on the always
1800’2017: 16.12.11 Always property
Implicit form:__
implicit_always: assert property(p);

Explicit form:
initial explicit_always: assert property(always p);
1800 also states “This is not shown as a practical example, but only for illustration of the meaning of always.”
The always needs a leading clocking event (LCE) prior to the always construct.
Thus,


module p;
  bit  clk, a ;
  always  #5  clk  =  !clk ;
  
  ap_illegal: assert property (always (@(posedge clk) a )); // line 5
// ** Error (suppressible): testbench.sv(5): (vlog-1957) 
//    The sva directive is not sensitive to a clock. Unclocked directives are not supported.
  ap_legal:   assert property (@(posedge clk) always (@(posedge clk) a));
  ap_legal2:  assert property (@(posedge clk) always (a) );
  initial begin
    #200 ;
    $finish();
  end
endmodule
6

In reply to ben@SystemVerilog.us:

Hi Ben,

Why did you use 2^31 for repetition value in the above equation? How does that number signify end of sim?

Thanks!!