In reply to Adarsh Santhosh: Requirements The start and end are starting and ending sections of simulation.
And, the signal TB.a is high between start and end with TB.clk pulsing.
There are better ways to express your requirements.
module m;
bit clk, start, done, a;
// The start and done are starting and ending sections of simulation.
// And, the signal TB.a is high between start and done with TB.clk pulsing.
//
// 1) PREFERRED PROPERTY STATEMENT BECAUSE:
// * ap_preferred has ONE attempt
// * Upon a start, "a" remains hi until done
initial ap_preferred: assert property(@(posedge clk)
start[->1] |=> strong(a[*1:$] intersect done[->1] ));
// Also OK
initial ap_preferred_OK: assert property(@(posedge clk)
start[->1] |=> a s_until done);
// ALso OK
initial ap_preferred_with_OK: assert property(@(posedge clk)
start[->1] |=> a s_until_with done);
// 2) Assertion with unnecssary multiple threads and
// issues with the disable
property Test1;
@(posedge clk) disable iff (start || done)
a |=> always(a);
endproperty
ap_TEST1: assert property(Test1);
// ap_TEST1 is disable when start and done occurs
// ap_TEST1 has an attempt at every clocking event.
// If a==1, then a new thread is started, and every started thread
// checks that a==1 at every clock. Thus, if you have 100 clocks
// you end up with 100 separate threads, and each threads checks that
// taht a==1. Consider the checks
// cycle 1 2 3 4 5 .... 100
// Thread1 a a a a a .... a
// thread2 a a a a .....a
// thread3 a a a .....a
// thread 100 a
// If you insist on using the always
// Syntax
// $past ( expression1 [, [number_of_ticks] [, [expression2] [, [clocking_event]]] ] )
property Test_better;
@(posedge clk) disable iff ($past(done, 1, 1, @(posedge clk)))
start[->1] |=> always(a);
endproperty
initial ap_TEST_better: assert property(Test_better);
initial forever #10 clk=!clk;
initial begin
repeat(10) @(posedge clk);
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: * Component Design by Example https://rb.gy/9tcbhl
* Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
* A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- Reflections on Users’ Experiences with SVA
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
- SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/
In reply to ben@SystemVerilog.us:
Lets say during the “end/done” section, signal “a” is “0” and i wanted to check if it says low for rest of the sim.
Looks OK
// Assertion states that in the cyce following done, and thereafter the done, a==0 until end of sim
// CORRECTION ********
initial ap_preferred: assert property(@(posedge clk)
done[->1] |=> strong(!a[*1:$])); // THIS IS INCORRECT because
// after the 1st !a the consequent completes.
// What you need
initial ap_preferred: assert property(@(posedge clk)
done[->1] |=> s_always (!a) );
// Assertion states that in the cyce following done, and thereafter the done, a==0 until end of sim
initial ap_preferred: assert property(@(posedge clk)
done[->1] |=> strong(!a[*1:$]));
I had some follow up questions.
What if there can be a delay in “a” going low after done.
a can be “0” in next cycle or any of the upcoming cycles.
Will below work?
// Assertion states that in any of the cycles following done : "a" is low, and thereafter, a==0 until end of sim
initial ap_preferred: assert property(@(posedge clk)
done[->1] |=> strong( !a[->1] ##1 !a[*0:$]));
I made the following correction above, my apologies
// Assertion states that in the cycle following done, and thereafter the done, a==0 until end of sim
// **** CORRECTION ****
initial BAD_ap: assert property(@(posedge clk)
done[->1] |=> strong(!a[*1:$])); // THIS IS INCORRECT because
// after the 1st !a the consequent completes.
// **** OK **** What you need
initial ap_preferred: assert property(@(posedge clk)
done[->1] |=> always (!a) );
// ON your other question
done[->1] |=> strong( !a[->1] ##1 !a[*0:$]));
// DO THIS instead
// At initialization, when done then starting from the next cycle
// wait for an occurrence of "a".
// In the cycle following the "a", that variable is always ZERO.
// SYntax:
property_expr ::=
... // several options, see 1800
| sequence_expr #-# property_expr // the followed-by operator.
| sequence_expr #=# property_expr
// property that follows a sequence by zero ( the #-#) or one cycle (the #=#) delay,
// starting from the end point of the sequence
| always property_expr
| always [ cycle_delay_const_range_expression ] property_expr
| s_always [ constant_range] property_expr
// Thus, the s_always require a range
module m;
bit clk, done, a;
initial
ap_1: assert property(@(posedge clk)
done[->1] |=> !a[->1] #=# always !a);
endmodule
In reply to Adarsh Santhosh:
// ON your other question
done[->1] |=> strong( !a[->1] ##1 !a[*0:]));
// DO THIS instead
done[->1] |=> s_always( !a[->1] ##1 !a[*1:]));
Hi Ben,
Can you share syntax of s_always?
Im getting an expected left bracket [ error at s_always.
In reply to Adarsh Santhosh:
Glad that you brought this up. I relied on memory.
In addition, I also made a mistake, particularly since I
am not an active user of SV and SVA.
As in any language, no use → it fades :)
OK, let’s get this assertion correctly.
// At initialization, when done then starting from the next cycle
// wait for an occurrence of "a".
// In the cycle following the "a", that variable is always ZERO.
// SYntax:
property_expr ::=
... // several options, see 1800
| sequence_expr #-# property_expr // the followed-by operator.
| sequence_expr #=# property_expr
// property that follows a sequence by zero ( the #-#) or one cycle (the #=#) delay,
// starting from the end point of the sequence
| always property_expr
| always [ cycle_delay_const_range_expression ] property_expr
| s_always [ constant_range] property_expr
// Thus, the s_always require a range
module m;
bit clk, done, a;
initial
ap_1: assert property(@(posedge clk)
done[->1] |=> !a[->1] #=# always !a);
endmodule
whats the difference between #1 and #=# . Does the second option mean 0 or 1? if so, wouldnt ##0 be sufficient. Since, we have only signal “a” of interest.(“a” goes low and “a” stays low)
since, we cant use s_always. How can we get a strong fail? Lets say “a” going low in consequent never happens.
whats the difference between #1 and #=# . Does the second option mean 0 or 1? if so, wouldnt ##0 be sufficient. Since, we have only signal “a” of interest.(“a” goes low and “a” stays low)
!a[->1] #=# (always !a); // is a property composed of the
sequence !a[->1] // and the
property (always !a)
!a[->1] ##1 (always !a) // is illegal
You can use the #=# to have a sequence followed by a property
Same thing for
sequence #0 property // ILLEGAL
sequence #-# property // LEGAL>
since, we cant use s_always. How can we get a strong fail? Lets say “a” going low in consequent never happens.
The s_always needs a range. Thus,
!a[->1] #=# s_always[0:$] !a); /// IS OK, s_always by itself is not OK
From LRM:
Ranged form of strong always
s_always [ constant_range ] property_expr
A property s_always [constant_range] property_expr evaluates to true if, and only if, all current
or future clock ticks specified by constant_range exist and property_expr holds at each of these
clock ticks. The range for a strong always shall be bounded
From my sim, it looks like if the range doesnt exist, it will fail.
In reply to Adarsh Santhosh:
Yes on “As per my understanding, any change in signal should act as trigger. can the signal be multibit?”
But if TN.state wil introduce other issues in the assertion. For example:
module m;
bit[3:0] a;
bit clk, b, c;
initial forever #5 clk=!clk;
always @(posedge clk) begin
a <= 1+1; b <= !b; c<=a[2];
end
ap_1: assert property(@(a) b|-> c);
initial begin
#100;
$finish;
end
endmodule
Here, in ap_1, the sampled value of b is not the one preceding the posedge of clk (in the preponed region). That’s because a changes in the NBA region, which is also where all the b and c also changes; the order of changes is not guaranteed.
You are asking for trouble.
I was wrong in how the simulator works for something like:
// signals a,b, and c are nonblocked assigned using posedge clk
ap_1: assert property(@(a) b[->1] !c s_until (a == 'd1000));
Above simulates OK even though a changes in the NBA region.
I am currently writing a paper on this, but it is not yet completed.
Generally, the preferred approach is:
ap_1: assert property(@(posedg clk) $changed(a) |-> b[->1] ##0 !c s_until (a == 'd1000));
I generally avoid the until unless the LHS is a simple expression rather than a sequence.
see my paper Reflections on Users’ Experiences with SVA, part 2 Reflections on Users’ Experiences with SVA, Part II