Hi!
I’m new to assertions and I cannot figure out how to write one assertion.
I want to finish assertion if one of sequences fails or pass.
Example:
wire A;
// seq_a and seq_b are some sequences
property;
$rose(A) |-> seq_a or seq_b
endproperty
As I’m correct each sequence has its own length and if seq_a fails but seq_b is still in progress then assertion is not finished untill seq_b is finished. And if it is finished with success then the result is 1. So whole property will success.
But I want next flaw:
if seq_a fails before seq_b finished then the result must be fail.
If seq_a success before seq_b finished then the result must be success.
If seq_b is finished and seq_b is still in progress and is not faild then result must by success
If seq_b fails then result of seq_a is assumed
Could someone could give me a clue what relation between this 2 sequences should be to get the workflow that I have described?
In reply to omehed:
Below is work-in-progress in that I initially used the sync_reject_on sync_accept_on, however,
1800’2017:16.12.14 Abort properties
The abort conditions may contain sampled value functions (see 16.9.3). When sampled value functions other than $sampled are used in the abort condition, the clock argument shall be explicitly specified. Abort conditions shall not contain any reference to local variables and the sequence methods triggered and matched.
I offer it here, though it is illegal, to provide something for discussion.
module m;
bit clk, a, b, reset_n=1'b1;
initial forever #10 clk=!clk;
wire A;
// seq_a and seq_b are some sequences
property P;
$rose(A) |-> seq_a or seq_b
endproperty
sequence seq_a; @ (posedge clk) a ##[1:3] b; endsequence
sequence seq_b; @ (posedge clk) a ##[1:6] b; endsequence
//As I'm correct each sequence has its own length and if seq_a fails
// but seq_b is still in progress then assertion is not finished untill seq_b is finished.
// And if it is finished with success then the result is 1. So whole property will success.
//
// sync_accept_on ( expression_or_dist ) property_expr
// reject_onsync_reject_on ( expression_or_dist ) property_expr
//But I want next flaw:
// (1) if seq_a fails before seq_b finished then the result must be fail.
/* NOTE: 1800'2017:16.12.14 Abort properties
The abort conditions may contain sampled value functions (see 16.9.3). When sampled value functions other
than $sampled are used in the abort condition, the clock argument shall be explicitly specified. Abort
conditions shall not contain any reference to local variables and the sequence methods triggered and matched. */
ap_1_ILLEGAL: assert property(@ (posedge clk) disable iff (!reset_n)
sync_reject_on ( seq_a.triggered )
$rose(A) |-> (seq_a) or seq_b);
// (2) If seq_a success before seq_b finished then the result must be success.
ap_2_ILLEGAL: assert property(@ (posedge clk) disable iff (!reset_n)
sync_accept_on ( seq_a.triggered )
$rose(A) |-> (seq_a) or seq_b);
// (3) If seq_a is finished and seq_b is still in progress and is not failed then result must by success
// (seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
ap_3: assert property(@ (posedge clk) disable iff (!reset_n) $rose(A) |->
(seq_a) within seq_b);
// (4) if seq_b fails then result of seq_a is assumed
ap_4: assert property(@ (posedge clk) $rose(A) |->
not(seq_a) and seq_b);
// ALL four cases
ap_1234_ILLEGAL: assert property(@ (posedge clk) disable iff (!reset_n)
sync_reject_on ( seq_a.triggered ) // case 1 <<--- BUT
sync_accept_on ( seq_a.triggered ) // COntradictory (case 2 and case 1)
$rose(A) |-> (seq_a or seq_b) or // case 1, 2
(seq_a within seq_b) or // case 3
(not(seq_a) and seq_b)); // case 4
endmodule
In reply to ben@SystemVerilog.us:
As explained above, 1800’2017 does not allow the use of endpoints in the use of sync_accept_on sync_reject_on
An option to write an assertion for something like that is to us tasks, as described in my paper Understanding the SVA Engine Verification Horizons - July 2020 | Verification Academy
Remember that an assertion is a confirmation that a statement is true. SVA is just an assertion language, but other techniques can be used to verify an assertion.
Below is my untested approach. Hopefully you will be able to follow it or updated to your needs.
module m;
bit clk, a, b, c, reset_n=1'b1;
initial forever #10 clk=!clk;
wire A;
sequence seq_a; @ (posedge clk) a ##[1:3] b; endsequence
sequence seq_b; @ (posedge clk) a ##[1:6] c; endsequence
//But I want next flaw:
// (1) if seq_a fails before seq_b finished then the result must be fail.
//ap_1_ILLEGAL: assert property(@ (posedge clk) disable iff (!reset_n)
// sync_reject_on ( seq_a.triggered )
// $rose(A) |-> (seq_a) or seq_b);
always_ff @(posedge clk) begin
fork
t_p1a();
t_p1b();
join_none
end
// sync_reject_on ( seq_a.triggered )
// $rose(A) |-> (seq_a) or seq_b);
task automatic t_p1a (); // the reject
bit pass_seq_a, pass_seq_b, done_a, done_b;
if($rose(A)) begin // $rose(A) |-> (seq_a) or seq_b);
fork
tseq_a(pass_seq_a, done_a);
tseq_b(pass_seq_b, done_b);
join_any
if(!done_b && done_a && pass_seq_a) // sync_reject_on ( seq_a.triggered )
p_reject_p1: assert(0)
else $display("%t p1 failed by rejection", $realtime);
end
endtask
task automatic t_p1b (); // without the reject
bit pass_seq_a, pass_seq_b, done_a, done_b;
if($rose(A)) begin // $rose(A) |-> (seq_a) or seq_b);
fork
tseq_a(pass_seq_a, done_a);
tseq_b(pass_seq_b, done_b);
join
p_pass1: assert(pass_seq_a || pass_seq_b)
else $display("%t p1 failed by ORing", $realtime); // (seq_a) or seq_b);
end
endtask
task automatic tseq_a (ref bit pass, done); // a ##[1:3] b;
pass=0;
if(a) begin
for (int i=1; i<=3; i++ ) begin
if(b) begin pass=1'b1; break; end
end
done=1'b1;
end
endtask
task automatic tseq_b (ref bit pass, done); // a ##[1:6] c;
pass=0;
if(a) begin
for (int i=1; i<=6; i++ ) begin
if(c) begin pass=1'b1; break; end
end
done=1'b1;
end
endtask
endmodule