Hello,
I want to write assertion for following scenario :
i have signal “a”,“clk”,“clk150”
->whenever signal a is high, my “clk” should toggle.(frequency of this “clk” is unknown)
->clk150 has frequency of 150MHz
->$changed won’t work because frequency of my “clk” signal is unknown so can’t check with respect to clk150
Thanks in advance
In reply to TRUSHAL:
If you rephrase your requirements, the assertion is trivial.
I read the requirements as : If a==1 there can be toggling
module m;
bit a, clk;
int err;
initial forever #5 clk = !clk;
ap_1: assert property (@(clk) strong (a)) else err=err+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
repeat (6) @(posedge clk) randomize(a);
#100;
$finish;
end
endmodule
of clk.
ap_clk: assert property(@(clk) a)
count=count+1; // count is for debug
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to TRUSHAL:
// create an event to detect when signal 'a' goes high
event a_high;
always @(a) begin
if (a) a_high = 1;
end
// create an event to detect when 'clk' changes
event clk_changed;
always @(posedge clk) clk_changed = 1;
// create an assertion to check that 'clk' toggles when 'a' is high
always @(a_high or clk_changed) begin
if (a_high)
assert(clk_changed) else $error("clk did not toggle when a was high");
end
// Create an assertion to check that clk150 has a frequency of 150 MHz
property freq150;
(clk150) |-> freq150;
freq150 = #1 (clk150);
endproperty
always @(posedge clk150) begin
assert(freq150==150MHz) else $error("clk150 does not have a frequency of 150MHz");
end
In reply to ben@SystemVerilog.us:
Hi Ben ,
Honestly speaking I didn’t get the question.When I went through this question , I thought the following one could be one of the possible ways.
property check;
@(posedge clk150) strong(a) |-> (clk != $past(clk,1));
endproperty
Then I noticed that the operation cannot be done with respect to clk150, couldn’t understand why?
Now there are only two signals we can take into our consideration : signal-a and signal-clk. I am trying to make the signal-a reference signal.
property check;
@(posedge a) (clk!=$past(clk,1));
endproperty
Hope this one makes something meaningful.
In reply to Shubhabrata:
In reply to ben@SystemVerilog.us:
Hi Ben ,
Honestly speaking I didn’t get the question.When I went through this question , I thought the following one could be one of the possible ways.
property check;
@(posedge clk150) strong(a) |-> (clk != $past(clk,1));
endproperty
Then I noticed that the operation cannot be done with respect to clk150, couldn’t understand why?
property_expr ::=
sequence_expr
| strong ( sequence_expr )
| weak ( sequence_expr )
...
@(posedge clk150) (a) |-> (clk != $past(clk,1));
says that when a is sampled with posedge of clk150 and a==1 then the previous sample of “a” at the posedge of clk150 was 0.
Now there are only two signals we can take into our consideration : signal-a and signal-clk. I am trying to make the signal-a reference signal.
property check;
@(posedge a) (clk!=$past(clk,1));
endproperty
Hope this one makes something meaningful.
@(posedge a) (clk!=$past(clk,1)); says
at every posedge of “a”, the sampled value of clk is unequal to it previous sample.
Thus, if always at a==0 or at a==1 (i.e, it does not change) then assertion is never triggered.
It does not check that when a==1 the clk toggles.
My original assertion of
ap_1: assert property (@(clk) strong (a)) else err=err+1;
states that at every clk change the value of a is equal to 1.
Again, you need to clarify your requirements.
Ben