Assert ack1 happened between req1 and req2

SystemVerilog
,
1

I have a question, I need to write an assertion to verify if $rose(ack1), there is definitely a $rose(req1) before and a $rose(req2) after, which is req1->ack1->req2. But if ack1 does not rise, req1, and req2 doesn’t need to follow this sequence.

I want to write:
property a_b_c;
@(posedge clk)
rose(req1)##[1:] $rose(ack1) |-> rose(ack1) ##[1:] $rose(ack2)
endproperty

But I think I am not correct. Any advice appreciated. Another dumb question is… I understand $rose means looking at the lsb bit change, but in this case, is there a difference to use rose or not?can I simply say: req1 ##[1:] ack1 |->ack1 ##[1:$] ack2

thanks in advance.

2

In reply to charlie.zl:

  • Structre: Read my response at
    Assertion attempt getting incomplete | Verification Academy
    rose(req1)##[1:] $rose(ack1) |-> …
    "Multi-thread sequences in both antecedent and consequent
    Should change that o either one of these:
    first_match(rose(req1)##[1:] $rose(ack1)) |-> …
    $rose(req1)## $rose(ack1)[->1] |-> …
  • rose(req1)##[1:] $rose(ack1) |-> rose(ack1) ##[1:] $rose(ack2)

// Is the ack in the same cycle as the request? If so
$rose(req1)## $rose(ack1)[->1] |-> strong(##[1:$] $rose(ack2))
// The  $rose(ack1) is redundant in the consequent.
  • is there a difference to use $rose or not?
    Absolutely! From my SVA Handbook on attempts:
    When the assertion is attempted at its leading clocking event, it is considered as a start event, represented as a blue square. In essence, an attempt is the start of an evaluation of an assertion (see 2.3.1 for more information on attempts). Assertion statements are started (attempted) at every leading clocking event, unless they are disabled or if they are turned off. If the attempt succeeds, one or more threads for that successful attempt are started, and those threads are independent from previous or future attempts. If the attempt fails, that assertion for that attempt is either vacuous if the property has an implication operator, or it fails if there is no implication in the property.
    Thus, without the $rose, The req1 ## … |-> consequent will be successfully attempted at every cycle req1==1’b1, and that can lead to errors. Consider:

ap: assert property(@ (posedge clk) a |=> b ##1 c );
a         0  1  1  0  0
b         0  0  1  0  0
c         0  0  0  1  0
Thread1   -  S  a  P
Thread2   -  -  S  F
S==Started, a==active, P==Pass, F==Fail

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

In reply to ben@SystemVerilog.us:

Thanks Ben, I agree with you that I have 2 follow up question:

ap: assert property(@ (posedge clk) a |=> b ##1 c );
a 0 1 1 0 0
b 0 0 1 0 0
c 0 0 0 1 0
Thread1 - S a P
Thread2 - - S F
S==Started, a==active, P==Pass, F==Fail

1, Let’s change the question a little bit. If a should be just 1 clock cycle. thread 2 will not be started. So in this case, using $rose and not will be the same, correct? If one day, someone told me, a is just one clock cycles, but there is a bug and it is actually 2 cycles. And if I use a |=> b ##1 c, it will fail by detecting as a by-product. Do you think it is a good idea? The only side effect is this way will make debug more confusing but it will save one assertion? I am a beginner, so do you think this is good? Or do you prefer keeping the $rose but adding another assertion to determine whether a is 1 clock or not?

2, Second question, you answer is exactly what I am looking for, but let’s get back to original assertion with some extension, now:
req1: | |____________________________________________
ack1:| || |______________
req2: ________________________________________| |

But actually what should happen is:
req1: | || |____________________________________________
ack1:| || |__________
req2: ________________________________________| || |

This time, I am trying to have an assertion where each ack1 will have its corresponding req1 and req2. My understanding is, if I use the exsiting solution: $first_match will look at the first pulse of req1, and first pulse of ack1(ignore second pulse ack1) in wave1. In wave2, assertion will look at (1st req1 & 1st ack1 -->1st_req2), then it will match (2nd req1 & 1st ack1–>1st req2)

I was wondering if there is a way to write an assertion based on the wave2 situation? which is where there is a ack1, there should be a dedicate req1 before and a req2 after, delay is still [1:$]？
1st req1 -->1st ack1–> 1st req2;
2nd req1 -->2nd ack1–> 2nd req2;

I just couldn’t find a good way to describe this situation. Is it possible/impractical to do that?

thanks in advance

4

In reply to charlie.zl:

In reply to ben@SystemVerilog.us:
1, Let’s change the question a little bit. If a should be just 1 clock cycle. thread 2 will not be started. So in this case, using $rose and not will be the same, correct? If one day, someone told me, a is just one clock cycles, but there is a bug and it is actually 2 cycles. And if I use a |=> b ##1 c, it will fail by detecting as a by-product. Do you think it is a good idea? The only side effect is this way will make debug more confusing but it will save one assertion? I am a beginner, so do you think this is good? Or do you prefer keeping the $rose but adding another assertion to determine whether a is 1 clock or not?

(a |=> b ##1 c) does not guarantee that “a” is a single pulse. It is very possible that if “a” is true for 2 or more cycles that all the attempts (in cycle 1, 2, and 3) succeed if the sequence (b ##1 c) matches for each of those attempts. Take the case where b==1 and c==1 in a dc manner (at all times).
Why are you stingy on assertions. If “a” is a MUST single cycle, then you need to verify that requirement,

2, Second question, you answer is exactly what I am looking for, but let’s get back to original assertion with some extension, now:
req1: | |____________________________________________
ack1:| || |______________
req2: | |
But actually what should happen is:
req1: | || |____
ack1:| || |__________
req2: ________________________________________| || |
This time, I am trying to have an assertion where each ack1 will have its corresponding req1 and req2. My understanding is, if I use the exsiting solution: $first_match will look at the first pulse of req1, and first pulse of ack1(ignore second pulse ack1) in wave1. In wave2, assertion will look at (1st req1 & 1st ack1 -->1st_req2), then it will match (2nd req1 & 1st ack1–>1st req2)

I addressed that topic of Uniqueness in attempted threads in my SVA Handbook Basically, need to assure that each started assertion from start to completion is unique; this means that if multiple assertions are started at different cycles because of a successful antecedent, a successful consequent should not terminate all those assertions. Below is a link to those pages from my book that explains the solution.

If you have any questions after you read section 10.26 Uniqueness in attempted threads – the FIFO, let me know.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. 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
5

In reply to ben@SystemVerilog.us:

OK, Thanks Ben, I will read those part. Thank you for your time!