I have a question on the assertion writing and verification using System Verilog.
Here is the case that I want to check
Signals a,b,c, have a sequence of a rise → b rise → c rise → c fell → b fell → a fell.
I want to make sure the time gap between a rise → b rise is more than 5 ns, b rise → c rise is more than 6 ns, c rise → c fell is more than 7 ns, c fell → b fell is more than 8 ns, b fell → a fell is more than 10 ns.
___________________________________
a _________________| |____________________
5ns _________________ 10ns
b _______________________| |_________________________
6ns _______ 8ns
c ___________________________| |________________________________
7ns
How would you write the assertion check?
And I want the assertion to be off if a fell before b/c rise, or b fell before c rise, which means any thing that happens before the sequence was fully completed, it will cancel the assertion, which means the assertion didn’t successfully complete. And if the timing requirement of the sequences are not followed, the assertion will flag error.
Could anyone please provide assertion code for the above case?
In reply to ianwyb:
Part of your requirements can be expressed as shown below:
property p_abc;
realtime t;
disable iff(0)
@(posedge a) (1, t=$realtime) |->
@(posedge b) ($realtime-t >= 5ns, t=$realtime) |->
@(posedge c) ($realtime-t >= 6ns, t=$realtime) |->
@(negedge c) ($realtime-t >= 7ns, t=$realtime) |->
@(negedge b) ($realtime-t >= 8ns, t=$realtime) |->
@(negedge a) ($realtime-t >= 10ns);
endproperty
ap_abc: assert property(p_abc);
Because you do not have a clock, there is a problem in defining a disabling condition.
Your disabling condition is the ORing of endpoints (the .triggered) of sequences.
SVA is really designed to work with clocking events that are based on clocks vs events that are bassed on data signals. If your design has the signals “a”, “b”, “c” generated off clocking events from clocks, then use those clocking events in your assertions.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
Thanks a lot for letting us know the assertions without the presence of clock.
Here in your solution, we nowhere monitor the stability of A or B or C right, If any of these signals change its state then we do not fail the assertions right ?
Overuse of the $stable, makes assertion harder to read.
($rise(a) ##1 $stable(a) [*5] is same as
($rise(a) ##1 a[*5])
Remember the definition of $stable:
$stable returns true if the sampled value of the expression did not change between the sampled value at the previous cycle and the sampled value at the current cycle. Otherwise, it returns false. $changed is a complement to $stable; $changed returns true if the sampled value of the expression changed.
2. Intersect of sequences that are 1 cycle is same as &&, thus
$stable(a) intersect $stable(b); is same as
$stable(a) && $stable(b);
Also, reconsider your need of use the $stable.
A sequence of (a ##1 $stable(a) && w) is same as
(a ##1 a && w). Why are you making it complicated?
Use of the implication operator. Keep in mind that if antecedent does not match, the property is vacuous.
On first_match(), it is needed in antecedents that have multiple possible matches. This happens with ranges (e.g., ##[1:5] or repetition e.g., w[*1:5], or sequences with the OR operator. You don’t have any of those.
Simplicity: Try to keep your assertions simple and easy to read. Multiple smaller ones are generally better than large complex assertions.
($rise(a) ##1 $stable(a) [*5] is **NOT** same as
($rise(a) ##1 a[*5]) right ??
Coz if ‘A’ makes a transition from 1 → 0 → 1 in between consecutive clk cycle (least possibility) then second one match but not the $stable(a) right ??
Or we don’t have to get into such a minute detail and can stick to simpler Assertions ?
In addition, w.r.t your solution, we only monitor the a-b-c edges and not its states after the transition, is it ok for this particular problem ??
@(posedge clk)($rise(a) ##1 $stable(a) [*5] is NOT same as
@(posedge clk) ($rise(a) ##1 a[*5]) right ??
Coz if ‘A’ makes a transition from 1 → 0 → 1 in between consecutive clk cycle (least possibility) then second one match but not the $stable(a) right ??
All variables are sampled. Thus, if ‘A’ makes a transition from 1 → 0 → 1 in between consecutive clk cycles, that transition will be missed, regardless of which sequence you pick. As I said, all variables are sampled!; what is in between the samples is irrelevant.
In addition, w.r.t your solution, we only monitor the a-b-c edges and not its states after the transition, is it ok for this particular problem ??
My solution does not rely on a clock, but on transitions, including glitches.
SVA was not intended for this, and a is based on clocks. However in my solution I used events, which is like a multiclocking scheme, and that works. Any glitch will create an event.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
Alright Ben, Thanks for correcting me.
But i guess i did not let you know my query in your solution I will put it here
property p_abc;
realtime t;
disable iff(0)
@(posedge a) (1, t=$realtime) |->
@(posedge b) ($realtime-t >= 5ns, t=$realtime) |-> // here we are waiting only for posedge-b event, lets say 'a' goes down and stays low for few ns
@(posedge c) ($realtime-t >= 6ns, t=$realtime) |->
@(negedge c) ($realtime-t >= 7ns, t=$realtime) |-> // and 'a' once again wakes up here or anywhere in between
@(negedge b) ($realtime-t >= 8ns, t=$realtime) |->
@(negedge a) ($realtime-t >= 10ns); // assumuing it will again fall here, our assertion will not fail but problem condition is not satisfied right ??
endproperty
ap_abc: assert property(p_abc);
My intent is only to get a solution in all the cases of a problem so trying to understand whether your solution will hold good in all the condition.
In reply to MLearner:
Only the conditions stated in the property are tested. Thus, if something is not stated, it is not validated. I prefer to write many small assertions instead of big ones, and SVA works best with variables sampled with clocking events. . You can have more than 1 clock.
Ben. SystemVerilog.us