property rdy2 ;
@( posedge clk ) $rose( rdy ) |-> ##[1:5] ack ;
endproperty
Property ’ rdy2 ’ checks that ’ ack ’ is received within 1 to 5 clock tick after ’ rdy ’ is asserted .
However if I receive multiple ’ ack ’ within 1 to 5 clock ticks the assertion would pass at the 1st ’ ack ’ .
I want to add an additional check that ensures that I receive exactly 1 ’ ack ’ per ’ rdy ’ within 1 : 5 clock ticks
If more than 1 are received then it should be a failure .
property rdy2 ;
@( posedge clk ) $rose( rdy ) |=> ack[=1] intersect 1[*5];
endproperty
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
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:
Hi Ben,
Could you pls explain the “intersect 1[*5]” part? Does this check for unique req-ack that OP seems to be asking for?
In reply to Aira:
// The ack[=1] is equivalent to.
!ack[*0:$] ##1 ack ##1 !ack[*0:$] // an infinite sequence
1[*5] // is a sequence that is true (that the "1") for 5 cycles
intersect // is the conjunction where those 2 sequences are common (true)
// so basically, the
intersect 1[*5] // defines the slice where
!ack[*0:$] ##1 ack ##1 !ack[*0:$] // is true.
Thus, the ack[=1] intersect 1[*5]; says there is one ack in 5 cycles.
An English equivalent: from a 100cm tape, look at the slice from 0cm to 5cm.
In harwware design, this is called an evaluation envelope.
In reply to ben@SystemVerilog.us:
Ben , two follow up questions
(1) Assume antecedent is True at Clock tick T0 , and the ’ ack ’ is received at T5
So the assertion would Pass at T5 .
I have following understanding of the consequent . Please correct me if wrong .
LHS of intersect operator is :: *( !ack[0:] ##1 ack ##1 !ack[*0:] ) .
It’s equivalent to ::
( !ack[*0] ##1 ack ##1 !ack[*0:$] ) or ( !ack[*1] ##1 ack ##1 !ack[*0:$] ) or
( !ack[3] ##1 ack ##1 !ack[*0:$] ) or ( !ack[*4] ##1 ack ##1 !ack[*0:$] ) or ....
( !ack[*0:$] ) is equivalent to ( !ack[*0] or !ack[*1] or !ack[*2] or .... )
So one such sequence from the infinite possible sequence is
( !ack[*4] ##1 ack ##1 !ack[*0] ) // This sequence is True for T1 to T5 .
As consequent has an implicit "first_match" , if any 1 of the infinite
combination is True the LHS of ' intersect ' operator is True .
(2) Is the above solution an alternative to your unique solution in :: Uniq_Ack
In reply to hisingh:
on #1:
ack[=1] intersect 1[*5]; would be the same as those five options
!ack[*0] ##1 ack ##1 !ack[*4] or // same as: ack ##1 !ack[*4]
!ack[*1] ##1 ack ##1 !ack[*3] or
!ack[*2] ##1 ack ##1 !ack[*2] or
!ack[*3] ##1 ack ##1 !ack[*1] or
!ack[*4] ##1 ack ##1 !ack[*0] // Same as: !ack[*4] ##1 ack
(2) Is the above solution an alternative to your unique solution in :: Uniq_Ack
NO. What happens is the antecedent is a match in cycle 1, 2, 3 and ack is true in cycle 5?
The assertion for those 3 attempts would pass in t5.
The uniqueness thing that you are referring in the link checks that if you have an ack, there was only a single request for it, ulike have 3 requests satisfied by a single ack
// code from the link
always @(posedge clk) begin
if(req && !ack) req_count <= req_count + 1; // was if(req) ... * 1'b1
if(ack && !req) req_count <= req_count - 1; // was if(ack) ... - 1'b1
end
sequence s_req; @(posedge clk) $rose(req) ##[0:5] 1'b1; endsequence // endpoints at 0, 1, ..5 cycles after req
ap_ack2req: assert property(@(posedge clk) $rose(ack) |-> req_count > 0 && s_req.triggered);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
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:
Ben ,
I tried both codes :: EDA1 and EDA2 .
For EDA1 , the single ’ ack ’ is considered a Match for ALL 3 antecedents .
[ Q1 ] What if I want an additional check that there Must be 1 ’ ack ’ per ’ req ’ ?
Similarly for EDA2 , the single ’ ack ’ is considered a Match for ALL 3 requests .
[ Q2 ] Similarly I would like to add an additional check that there Must be 1 ’ ack ’ per ’ req ’
So if remaining 2 ’ ack’s ’ aren’t received in both code I should see the assertion Fail twice
In reply to hisingh:
For Q1 and Q2 you would need support-logic. Here are 2 links that can provide examples.
https://verificationacademy.com/forums/systemverilog/grant-must-some-time-have-been-preceded-request#reply-104623
You can also add counters on those req ack and use those values in the assertions.
On Q2, you need to task the req. See my replies
https://verificationacademy.com/forums/systemverilog/assertion-req-and-gnt-signals
In reply to ben@SystemVerilog.us:
Ben ,
I tried the following based on the 2nd link you shared :: Uniq_ack_for_Each_Request
However in the stimulus although I received 3 ack’s the assertion still fails
In reply to hisingh:
By doing the cover to address the increment of the now_serving also increments the ticket
thru the inc_ticket()
Thus, your ticket counter went something like 2, 4, 6, 8 instead of 1, 2, 3, …
You don’t need the cover statement, the assert st does that anyway.
And why split the increment of those counters in 2 places?
property reqack_unique;
int v_serving_ticket;
@(posedge clk) ( $rose(rdy), v_serving_ticket = ticket , inc_ticket() ) |->
strong( (( now_serving == v_serving_ticket ) && ack ) [ ->1 ]) ;
// ================================================================
endproperty
a_property : assert property ( reqack_unique )
now_serving =now_serving+1; else begin // pass or fail, need to increment now_serving
now_serving = now_serving + 1 ; // Increment for Each Pass / Fail
$display(" TIME : %0t AB FAIL " , $time ) ;
end
/* Doing the cover to increment the now serving also increments the ticket
thru the inc_ticket()
c_property : cover property ( reqack_unique )
begin
now_serving = now_serving + 1 ; // Increment for Each Pass / Fail
$display(" TIME : %0t AB PASS " , $time ) ;
end */
In reply to ben@SystemVerilog.us:
Ben ,
Thanks for the explanation .
Without the cover property the assertion works as intended .
Added another assertion as per Ack_should_be_preceded_with_request to throw errors for extra ’ ack ’ violations .
Have a few follow up questions ::
(1) The reason I added cover property is to ensure vacuous pass reports are not shown via assert property
[Q1] How is that if $rose( rdy ) is False there is No Vacuous pass report via ’ assert property ’ ?
Also will the assignment N subroutine call occur ONLY when $rose( rdy ) has Non - vacuous pass ?
(2) I was referring to SV LRM 2017 , Section 16.11 , Syntax 16-15
sequence_expr ::= // from A.2.10
...
| ( sequence_expr {, sequence_match_item} ) [ sequence_abbrev ]
...
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call
The antecedent has 3 parts in your solution .
(a) Sequence Expression :: $rose( rdy )
(b) Assignment
(c) Subroutine call .
I also notice that instead of the subroutine call , if I were to write the increment as 3rd part I get compilation error .
[Q2] Is the order fixed i.e assignment should be written before subroutine call ? . Can we have more than 3 parts too ?
I have seen codes with multiple assignments ::
sequence dataCheck ;
int ldata1 , ldata2 ;
( rdc , ldata1 = rData , ldata2 = retryData ) ##5 ....
// ' rdc ' is another sequence .
endsequence
[Q3] This was an application of a subroutine call from an expression .
What other cases can we use the subroutine for ?
The book I am currently referring ( by Ashok Mehta ) has codes using it for debugging purposes ( To display reports )
and also hints that it could be used to collect coverage information too .
In reply to hisingh:
Added another assertion as per Ack_should_be_preceded_with_request to throw errors for extra ’ ack ’ violations .
Have a few follow up questions ::
(1) The reason I added cover property is to ensure vacuous pass reports are not shown via assert property
There are switches in tools to determine the information to be reported. Genratlly, tools report real pass/failures and vacuous passes.
[Q1] How is that if $rose( rdy ) is False there is No Vacuous pass report via ’ assert property ’ ?
Also will the assignment N subroutine call occur ONLY when $rose( rdy ) has Non - vacuous pass ?
(2) I was referring to SV LRM 2017 , Section 16.11 , Syntax 16-15
sequence_expr ::= // from A.2.10
...
| ( sequence_expr {, sequence_match_item} ) [ sequence_abbrev ]
...
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call
The antecedent has 3 parts in your solution .
(a) Sequence Expression :: $rose( rdy )
(b) Assignment
(c) Subroutine call .
I also notice that instead of the subroutine call , if I were to write the increment as 3rd part I get compilation error .
You are correct.
sequence_expr ::= …
( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ]
The sequence_match_item is only executed if the sequence_expr is a match colloquially called true, but sequences match or do not match. See my paper - Reflections on Users’ Experiences with SVA
Reflections on Users’ Experiences with SVA
As you stated, the following in a sequence_match_item:
sequence_match_item ::=
operator_assignment // example ($rose(a), local_variable1=sig1, local_variable2=sig2)
// ILLEGAL: ($rose(a), sig1=1'b1)
| inc_or_dec_expression // ($rose(a), local_variable1++)
| subroutine_call // ($rose(a), my_function(sig1), $display("%t sig1=%b, ...)
[Q2] Is the order fixed i.e assignment should be written before subroutine call ? . Can we have more than 3 parts too ?
I have seen codes with multiple assignments ::
sequence dataCheck ;
int ldata1 , ldata2 ;
( rdc , ldata1 = rData , ldata2 = retryData ) ##5 ....
// ' rdc ' is another sequence .
endsequence
( sequence_expr {, sequence_match_item } )
After the sequence_expr and if that matches then you can have multiple sequence_match_items
separated by a comma. The {} in the definition mean a repeat of what is in it.
NO order is specified, meaning you can have a local variable assignment followed by a function call, or vice versa. However, the items within the sequence_match_item are executed in order from left to right. Thus, in ($rose(a), v1=3, v2=4, v3=v1+v2) v3==7.
[Q3] This was an application of a subroutine call from an expression .
What other cases can we use the subroutine for ?
The book I am currently referring ( by Ashok Mehta ) has codes using it for debugging purposes ( To display reports )
and also hints that it could be used to collect coverage information too .
Subroutine calls are used in support logic and demonstrated by this example (e.g., increment the counters. Note that module variables can be directly modified in the action blocks.
In reply to ben@SystemVerilog.us:
I tried various examples from LRM Section 16.11 for better understanding .
I finally get the reason you called the subroutine to increment variable ’ ticket ’
( As ’ ticket ’ isn’t a local variable it can’t be assigned within the property )
I have a few more questions to conclude the thread :: EDALINK
Via +define+M_A ::
**[Q1] Both the $display() execute in the re-active region .
Is there a predefined order in which the $display() ( within the property V/S within the pass / fail action block ) should execute ?
i.e Should the $display() within the property execute before the Pass / Fail action block ??**
[Q2] Can I say the following ::
(a) The assignment to local variables ldata take place in re-active region .
(b) The local variables ldata are assigned the preponed Value sampled for rdata***
Via +define+M_S ::
[Q3] I observe that $display() within the property reports different values than the $display() executed within the subroutine .
Is it cause the preponed values are used in $display within the property ?
[Q4] Is there a defined order in which the $display() be executed within the subroutine , within the property and the pass / fail action block ?
In reply to hisingh:
In reply to ben@SystemVerilog.us:
…I have a few more questions to conclude the thread :: EDALINK
Via +define+M_A ::
[Q1] Both the $display() execute in the re-active region .
Is there a predefined order in which the $display() ( within the property V/S within the pass / fail action block ) should execute ?
i.e Should the $display() within the property execute before the Pass / Fail action block ??
[Ben]See diagram in SVA evaluation - SystemVerilog - Verification Academy
The Observed region is where the evaluation of the property expressions when they are triggered. That would include any function calls (user-defined functions or system functions, like $display). The action blocks are executed in the reactive region, after the Observed Region. Thus, your $display in the sequence_match_item would execute before a $display in the Action block.
[Q2] Can I say the following ::
(a) The assignment to local variables ldata take place in re-active region .
(b) The local variables ldata are assigned the preponed Value sampled for rdata*
[Ben] NO, what you say is not correct. local variable are executed where the property is executed, in the Observed region, see my diagram in the link above. Values of signals used in the assignment are the ones in the Preponed region. Thus,
($rose(a), v1=sig1) // In the Observed region, v1=sig1 value in the Preponed region.
**
Via +define+M_S ::
[Q3] I observe that $display() within the property reports different values than the $display() executed within the subroutine .
Is it cause the preponed values are used in $display within the property ?
[Q4] Is there a defined order in which the $display() be executed within the subroutine , within the property and the pass / fail action block ?
[/quote] See below
ap: assert property(@ (posedge clk) sig1 |-> sig2 );
else ($display("sig1 sampled %b, sig1 in Reactive region %b",
$sampled(sig1), sig1);
In reply to ben@SystemVerilog.us:
Should it be “within” instead of “intersect” ? as intersect requires both start and end of the sequences to be same
In reply to DVtrojan:
They ALL would work
ack[=1] intersect 1[*5];
ack[=1] within 1[*5];
ack[->1] within 1[*5];