I want to implement the following functionality using SVA, when my reg_value becomes 57, sample the counter value at that time. Then wait for the 4 concurrent events to occur(no particular order), for posedge of sig_1, negedge of sig_b, either edge for sig_c, logic high for sig_d. After all the event occurs, check on the next clock, if the counter has incremented by 1 while throughout this process it should remain constant.
/* I want to implement the following functionality using SVA,
when my reg_value (data) becomes 57, sample the counter value at that time.
Then wait for the 4 concurrent events to occur(no particular order),
for posedge of a, negedge of sig_b, either edge for sig_c, logic high for sig_d.
After all the event occurs, check on the next clock, if the counter has incremented
by 1 while throughout this process it should remain constant. */
Are signals a, b, c, d clocked?
module m;
bit clk, a, b, c, d;
int cntr, data;
always @(posedge clk) begin
if(data==32'h00000057)
fork t($sampled(cntr));
join_none
end
task automatic t(int ct);
fork
@(posedge a);
@(negedge b);
@(c);
wait(d==1);
join
@(posedge clk) assert(cntr==ct+1);
endtask // t
endmodule
Yes a, b, c are clocked. One follow up question : When data becomes 32’d57, then it will not change till the all the events are triggered, so is it necessary to fork the the task while you’re calling it? Because once data becomes 32’d57, in every posedge it will create another thread to check the events which is not required i think.
Modified version:
Does this seem correct to you?
Yes a, b, c are clocked. One follow up question :
When data becomes 32’d57, then it will not change till the all the events are triggered, so is it necessary to fork the the task while you’re calling it? Because once data becomes 32’d57, in every posedge it will create another thread to check the events which is not required i think.
- Since the full set of requirements were not fully described, I followed the SVA model where if the antecedent is a match the consequent is initiated. See my paper “Understanding the SVA Engine Using the Fork-Join Model”
Verification Horizons
Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.
[YOU] so is it necessary to fork the the task while you’re calling it?
[Ben] You can put flags to test and stop any refiring of the task t.
module m;
bit clk, a, b, c, d, go=1;
int cntr, data;
always @(posedge clk) begin
if(go && data==32'h00000057)
fork t($sampled(cntr));
join_none
go <= 0; // disable further triggers of task t
end
task automatic t(int ct);
fork
@(posedge a);
@(negedge b);
@(c);
wait(d==1);
join
@(posedge clk) assert(cntr==ct+1);
go <= 1; // enable further calls of task t
endtask // t
NOTE: SVA will not work in this case because of clock flow restrictions in ANDing of sequences
// Asserting on an illegal multiply clocked temporal expression. The clock flow cannot change in the RHS of 'and' operator.
/// https://www.edaplayground.com/x/TbJJ
property p1; // WILL NOT COMPILE
int v;
@(posedge clk) (data==32'h00000057, v=cntr) |->
(
(@(posedge a) 1) and
(@(negedge b) 1) and
(@(c) 1) and
(d[->1] )
) ##1 cntr==v+1;
endproperty
ap1: assert property(@ (posedge clk) p1);
Thanks Ben
Here is another suggestion if you want to use “and”
module test;
bit clk, a, b, c, d;
int cnt, data;
property pp();
(data==32'd57) |-> ($rose(a)[->1] and $fell(b)[->1] and $changed(c)[->1] and d[->1]) ##1 (cnt == $past(cnt)+1);
endproperty
as_pp : assert property (@ (posedge clk) pp);
always #1 clk = !clk;
initial begin : test_pattern
#5 data = 32'd57;
#4 d = 1;
#3 b = 1;
#2 c = 1;
#1 a = 1;
#3 b = 0;
// comment the next line and the assertion should fail
#1 cnt = 1;
end
initial begin
#100 $finish;
end
endmodule
That would work since you only have one clock.
Good soution.
Thanks,
Ben
1 Like
A reply to Ed Cerny, ref: LinkedIn Login, Sign in | LinkedIn
The use of the local variable is needed because the increment is related to the cntr;s original sampled value. There is a need in the requirements that cntr be stable during those ANDed cycles. So we need another assertion or something like.
property p;
int v;
@(posedge clk) (data==32'h00000057, v=cntr) |->
((
($rose(a)[->]) and
($fell(b)[->1]) and
($change(c)[->1]) and
(d[->1] )
) ##1 cntr==v+1) intersect
(cntr==v[*1:$] ##1 cntr==v+1);
endproperty