SV Assertions clock period

SystemVerilog
,
1

Hi,

I try to check clock period by SVA,
trying this code:

module spi_qspi_assertions (logic SCLK, time tclk);

time curr_time;

Tclk : assert property
@(posedge SCLK) ('1, curr_time = $time) |-> @(posedge CLK) (tclk == ($time - curr_time));

endmodule

I got an error:

image
image744×127 11.5 KB

I’ll be happy for explanation what is the start of the line meaning ( ('1, curr_time = $time))
and why I get this error?

Thanks

2

Hi,

I want to add my previous question:

What is the different between :

Tclk : assert property (('1, curr_time = $time) |=> (tclk == $time - curr_time));

and:

property Tclk (logic SCLK,time tclk);
time curr_time;
(('1, curr_time = $time) |=> (tclk == $time - curr_time));
endproperty
//@(posedge ass

Thanks a lot

3

You need to declare the local variable curr_time within the property declaration.
what you have above is illegal

property p_tclk;
  realtime curr_time;
@(posedge SCLK) ('1, curr_time = $time) |-> @(posedge CLK) (tclk == ($time - curr_time));
endproperty

ap_tclk : assert property (p_tclk);

// The following has formal arguments. 
property Tclk (logic SCLK,time tclk);
...

   Ben Cohen
   Ben@systemverilog.us
   Link to the list of papers and books that I wrote, many are now donated.
   https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
4

Thank a lot @hdlcohen ,

I want to try it.
could you please explain me, what is the mean in the last line?

// The following has formal arguments.
property Tclk (logic SCLK,time tclk);

in addition,
I need to assert the above assertion in a loop, somethink like (pseudo code)

@(posedge en)
repeat(20) begin
@(posedge CLK)
assert…
end

Thanks a lot.

5

could you please explain me, what is the mean in the last line?
// The following has formal arguments.
property Tclk (logic SCLK,time tclk);
The property has formal arguments that can be replace with actual arguments when you assert the property. I rewrote as follows:

logic sclk; 
realtime tclk_period=10ns; 
property p_Tclk (logic SCLK,  realtime tclk);
  realtime curr_time;
  @(posedge SCLK) ('1, curr_time = $realtime) |-> 
      @(posedge SCLK) (tclk == ($realtime - curr_time)); 
endproperty 
ap_Tclk: assert property(p_Tclk(sclk, tclk_period)  );

in addition, I need to assert the above assertion in a loop, something like (pseudo code)
@(posedge en) repeat(20) begin @(posedge CLK) assert… end
You probably mean that you need to instantiate this property with 20 separate assertions.
You can use the generate statement. Example:

module m; 
..
// Create 15 instances of this arbiter assertion for each indexed req and grnt.
   generate for (genvar i=0; i<=15; i++)
      begin
       property p_arbiter;
         bit[16:0] v;
         (req[i]==1'b1, v=0, v[i+1]=1'b1) ##0 req < v |->
         grnt[i]==1'b1 ##0 $onehot(grnt);
       endproperty : p_arbiter
       ap_arbiter: assert property(@(posedge clk) p_arbiter);
     end
  endgenerate

If this is not what you meant, please explain what you need.

6

Thanks @hdlcohen

7

wave_2024-08-18_14h09_02
wave_2024-08-18_14h09_02818×182 22.7 KB

During the simulation, I have 20 times, for example, that the CS fall, and I want to check the clock period,
So the code is:

property Tclk (time tclk);
time curr_time;
(('1, curr_time = $time) |=> (tclk == $time - curr_time));
endproperty
assert_period : assert property (@(posedge spi_qspi_vif.SCLK) Tclk(40ns))$display("Assertion assert_period Passed");
                else $display("Assertion assert_period Failed");

the problem is regard the last clock for each CS go down,
the assertion check the clock from posedge to posedge, and the last posedge of clock in one CS, failed in the assertion, because the next posedge in clock is in the next CS negedge, .
I try to avoid the last posedge clock in each CS negedge.
What about an assertion as follows:


bit cpol0, cpol1, cs; 
let period=40ns
property p_col0 (time prd);
  realtime curr_time;
@(negedge cs) 1 |-> (@(posedge cpol0) ('1, curr_time = $realtime) ##1
                      (prd == $time - curr_time)) [*8] ##0 
                      @(posedge cs) cpol0==0;
endproperty

property p_col1 (time prd);
  realtime curr_time;
@(negedge cs) 1 |-> (@(negedge cpol1) ('1, curr_time = $realtime) ##1
                      (prd == $time - curr_time)) [*8] ##0 
                      @(posedge cs) cpol1==1;
endproperty