Assertions - signal stability until a certain signal posedge

SystemVerilog
, ,
1

Hello,

I am writing an assertion and the idea is that i have a signal called PADDR which needs to be stable (not change) from the moment that it changes until the moment a signal PREADY transitions from 0 to 1. This is some code that i tried but the assertion never passes nor it fails. If anybody has some suggestions I would be very grateful.


  property stable_paddr;
    @(posedge PCLK)
    disable iff (!PRESETn)
    $changed(PADDR) |=> $stable(PADDR) [*1:$] ##1 PREADY;
  endproperty

  assert property(stable_paddr)
    `uvm_info("training_uvc_if","PADDR is stable here",UVM_MEDIUM)
  else
    `uvm_error("training_uvc_if","ERROR: PADDR changed during cycle!")
2

Your assertion looks OK unless you want the stability when PREADY==1.
2 options

 
property stable_paddr;
    @(posedge PCLK)
    disable iff (!PRESETn)
    $changed(PADDR) |=> 
        strong(first_match($stable(PADDR) [*1:$] ##1 $rose(PREADY)) ##0 $stable(PADDR));
  endproperty

// you can also consider the use of the s_unti_with

property stable_paddr2; // 
    @(posedge PCLK)
    disable iff (!PRESETn)
    $changed(PADDR) |=> 
               $stable(PADDR) s_until_with PREADY ##0 $stable(PADDR);
  endproperty

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
  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:

I forgot to explain that a master is driving the PADDR line and a slave is driving the PREADY line. When a transition occurs on the PADDR line, this triggers the slave to do some work and after a random number of PCLKs (bigger than 1) the slave gives a PREADY signal that lasts only one PCLK. So I need to check that the PADDR line is stable throughout the interval of time that beggins when a PADDR transition occurs until the PREADY signal becomes one, the whole time.

Here’s a URL to an image which demonstrates a cycle.

So if I understood you well, I have mistakenly written an assertion that just checks if PADDR is stable only when PREADY arrives (becomes 1) but not throughout the whole cycle?

4

In reply to Nikola Vulinovic:

The image URL didn’t appear for some reason…

https://ibb.co/Wvx1SLB

5

In reply to Nikola Vulinovic:

The assertions I rewrote are correc. A couple of comments:


property stable_paddr;
    @(posedge PCLK)
    disable iff (!PRESETn)
    $changed(PADDR) |=> 
        strong(first_match($stable(PADDR) [*1:$] ##1 $rose(PREADY)) ##0 $stable(PADDR));
endproperty
// The following is of the form 
(first_match(a[*1:$] ##1 b) ##0 c). 
// In your case, the c"c" is the "a", thus you don't need the first_match() because 
// if b==1 and a==0, the assertion will fail at the next cycle because of the  a[*1:$]
// However, I like to keep it clean and use the first_match() 

// Another observation from the diagram is that you can also write as 
property stable_paddr;
    @(posedge PCLK)
    disable iff (!PRESETn)
    $changed(PADDR) |=> 
        strong($stable(PADDR) [*1:$] ##0 $rose(PREADY));
endproperty

// The following is also OK, though the s_until_with requires some mental 
// evaluation as to its meaning 
property stable_paddr2; // 
    @(posedge PCLK)
    disable iff (!PRESETn)
    $changed(PADDR) |=> 
               $stable(PADDR) s_until_with $rose(PREADY); 
         // I was mistaken on the ##0 $stable(PADDR) in my prior answer since the 
         // s_until_with requires that $stable(PADDR)==1 when $rose(PREADY)==1
  endproperty

You stated that the assertion never passes nor it fails. Actually the assertion should fail if PADDR is changed and no Pready. It should also pass since the sequence is in the consequent and the search is for a pass. If $stable(PADDR) is ever equal to 0, there is no need for further searches because of the repeat. stable(PADDR) [*1:] requires no drop in $stable(PADDR). It is not like the range delay.


 a |=> ##[1:$] b; 
// can never fail because if b==0, there is a search for another ##1 b after b==0. 
// Assertion can pass though at the first occurrence of b

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
6

Thank you so much for the detailed explanation. Realy great!