“A signal should be high for a min of 3 and max of 5 non-consecutive cycles over 10 cycle period.”
I tried writing the following assertion:
$rose(a) |-> a[=3:5] and 1[*10];
is this correct? are there any better ways to express that assertion?
Thanks!
In reply to Koushik:
Looks almost OK: you need the intersect operator instead of the and operator.
Also, the $rose(a) |-> a[=1] will be true at $rose(a) because at rose(a) a==1.
Thus, your a[=3:5] will be equivalent to 2 to 4 more occurrences of “a”. Is this what you want? Or do you want 3 to 5 more occurrences of “a”?
$rose(a) |=> a[=3:5] intersect 1[*10]; //3 to 5 more occurrences of "a"
From my SVA Handbook 4th Edition
- and : non-length-matching sequence conjunction. The sequence operator and is used when both operands are expected to match, but the end times of the sequences can be different. A sequence and operator between two sequences starts two concurrent threads, one for each sequence; each sequence in turn can be mulit-threaded.
- intersect : length-matching sequence conjunction. The sequence operator intersect is used when both operands are expected to match, and the end-times of the sequences end in the same cycle. A sequence intersect operator between two sequences starts two concurrent threads, one for each sequence; each sequence in turn can be mulit-threaded
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
In reply to ben@SystemVerilog.us:
Thank you ben!
Yeah, I need a total of 3 to 5 occurrences including the first occurrence when $rose(a) happens.
So,
$rose(a) |=> a[=2:4] intersect 1[*10];
or
$rose(a) |-> a[=3:5] intersect 1[*10];
should be Ok.
In reply to Koushik:
I prefer this version, which also clarifies the range for the number of cycles.
$rose(a) |=> a[=2:4] intersect 1[*10]; // 10 more cycles after the rose(a)
// Shoud this be 1[*9] ??
//
// The following creates a mental exercise
$rose(a) |-> a[=3:5] intersect 1[*10];
// So that is 2 to 4 more, because it includes the antecedent term.
// Also, the 10 cycles is inclusive of the 1st term.
// Ah, so now I have to account how the |-> interplays ...
// am getting a headache!!!
// the |=> is clearer as to which cycles I mean.
BTW, I know SVA, but I stil had to go through this mental exercise ...
:)
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
So, everything on the right hand side(RHS) of “|=>” should start evaluating from the next cycle on which LHS is true right?
Then, as you said,
$rose(a) |=> a[=2:4] intersect 1[*9];
looks more correct in the lines of what I am thinking.
In reply to Koushik:
You are correct. From my SVA Handbook
Overlapped implication operator |->
Rule: The “|->”overlapped implication operator allows an if – then checking in a property. This operator specifies that if there is a match for the antecedent sequence_expr, the condition that follows the operator (i.e., the fulfilling condition or consequent) begins in the same cycle in which the end point of the antecedent becomes true.
Non-Overlapped Implication Operator |=>
Rule: For non-overlapped implication, the start point of the evaluation of the consequent property_expr is the clock tick after the end point of the antecedent. Therefore (and by definition):
sequence_expr |=> property_expr is equivalent to:
sequence_expr ##1 `true |-> property_expr
The above definition is important to understand because
sequence_expr ##1 `true |-> property_expr // is different than
sequence_expr |-> ##1 `true ##0 property_expr // consequent is not a property
// That consequent is a sequence followed by a property, which is illegal with the ##0 operator
Note: To express a consequent that occurs n or more cycles after the antecedent, it is more readable to use the overlapping implication operator; thus,
req |-> ##[1:4] ack; // More readable than
req |=> ##[0:3] ack; //
Your situation is different, and I prefer
$rose(a) |=> a[=2:4] intersect 1[*9];
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115