Assertion b high at least once

HI all,

I was trying to write down this assertion.

When enable == 1 I have to check that b is down once time at least when another signal a is high.
I wrote it with a counter, checking that it’s different from zero when enable goes down.

Is there a simpler way to implement this assertion?

I uploaded the assertion representation here:

In reply to dave_59:


 ap: assert property(@ (posedge clk)
      $rose(enable) |-> $fell(b) && a within $fell(enable)[->1]);   
 

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


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thanks ben! It’s what i was looking for!!

In reply to ben@SystemVerilog.us:

Hi Ben,

Does your solution restrict the check to the same cycle as enable signal rose or would it span multiple cycles until the first occurrence of $fell(b)?

Somehow, with the overlapping implication, I am misled into believing this wont work as intended. Could you kindly clarify?

In reply to kernalmode1:

In reply to ben@SystemVerilog.us:
Hi Ben,
Does your solution restrict the check to the same cycle as enable signal rose or would it span multiple cycles until the first occurrence of $fell(b)?
Somehow, with the overlapping implication, I am misled into believing this wont work as intended. Could you kindly clarify?


(seq1 within seq2) // is equivalent to: 
((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 ) //Thus, 
a |-> b within c[->1];  // equivalent to 
a |-> ((1[*0:$] ##1 b ##1 1[*0:$]) intersect 
      !c[*0:$] ##1 c) 
// if a==1, b==1, c==1 then for that attempt, above expression gets reduced to 
a|-> ( b ##1 1[*0:$]) intersect c; / or simply 
a |-> b inteeset c; // true in that attempt. 
// Now, for your case
 $rose(enable) |-> $fell(b) && a within $fell(enable)[->1]);   
// You CANNOT have a  $rose(enable) and a  $fell(enable) in the same cycle, thus 
// the check would span over multiple cycles until the first occurrence of $fell(b)?
// However, the following can occur in the same cycle since the $rose and $fell can occur in //the same cycle
$rose(enable) |-> $fell(b) && a within $fell(c)[->1]);
 

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


  1. https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. 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
    FREE BOOK: Component Design by Example
    … A Step-by-Step Process Using VHDL with UART as Vehicle

    http://systemverilog.us/cmpts_free.pdf