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:
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
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
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
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.
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.
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