Assertion for a signal to rise before an offset

SystemVerilog
, , , ,
1

Hi,

I have an assertion question.

In my assertion, an offset should determine how much earlier to send a signal prior to a signal with value incrementing in every clock cycle. Below is my assertion.

property delay_assert(a,offset,b);
int v,s;
@(posedge clk) disable iff(reset)
(rose(a), v= offset, s=b) |-> ((a,v=v-1)[*0:] ##1 (v==0 && s==s+1));
endproperty

The signal b value doesn’t match with the incrementing values in the waveform. I tried using $past as well but it doesn’t work. Any lead would be helpful.

2

In reply to sowmya.ragav:

Requiremens In my assertion, an offset should determine how much earlier to send a signal prior to a signal with value incrementing in every clock cycle.

That requirement is ambiguous. Do you mean to say:
Following the rise of signal “a”, the 32-bit signal “b” should be incremented after an offset of a number of system clocks. The value of that offset is stored in an 8-bit register. During that offset time, signal “a” shall remain in the logical high state.
With the above requirements, I would write:


property delay_assert(a,offset,b);
 bit[7:0] v_offset; 
 bit[[31:0] v_b;  
 @(posedge clk) disable iff(reset)
 ($rose(a), v_offset= offset, v_b=b) |-> 
   first_match((a,v_offset=v_offset - 1'b1)[*0:$] ##1 v_offset==0) ##0 
   $changed(b) && b==v_b+1'b1);
endproperty

I understand that you hastily wrote your requirements for the assertion for this forum. However, requirements really need to be better defined. For your benefit and this audience, I recommend that you take a look at my book (below) that goes ito great details about defining requirements and verification plans.
FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle

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. 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
3

In reply to ben@SystemVerilog.us:

Hi,
Thank you very much for your reply. I am sorry if my requirements were not clear. b is a signal which contains values incrementing from 0 to 10 and keeps repeating for the entire time. When the value of signal b changes, at that point signal a which is 1 bit should rise before an offset. rise of signal a should happen before every start time of values changing in signal b by an offset.

4

In reply to sowmya.ragav:

I believe my assertion does that. My rewrite of the requirements says what you expressed, but is forward looking

5

In reply to ben@SystemVerilog.us:

I tried your assertion but the value of b doesn’t change when offset becomes 0. Is there anyway I can find the change of b and check for signal a. I tried the below code too but it said illegal operand for constant expression

property delay_assert(a,offset,b);
@(posedge clk) disable iff(reset)
$changed(b) |-> ($past(a,offset)==1);
endproperty

6

In reply to sowmya.ragav:

Good solution with one big EXCEPTION!
$changed(b) |-> ($past(a,offset)==1);
Requires “offset” to be static and NOT dynamic. Thus


 int offset=7; 
 let static_offset=6; 
 $changed(b) |-> ($past(a,offset)==1); // ERROR !!!!
 $changed(b) |-> ($past(a,static_offset)==1);  // OK

As a general comment, the above styles of assertions is generally of poor style because it is not forward looking. It is saying if something happens, then something else before that must have happened. I pefer the forward looking approach that says, if something happens, then now or later on something else must happen. My solution does that:


($rose(a), v_offset= offset, v_b=b) |-> // something happens 
   first_match((a,v_offset=v_offset - 1'b1)[*0:$] ##1 v_offset==0) ##0 
    // after an offset time set dynamically when that something did happen
   $changed(b) && b==v_b+1'b1);  // 2 other things happen

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

  1. 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
    FREE BOOK: Component Design by Example
    … A Step-by-Step Process Using VHDL with UART as Vehicle
    http://systemverilog.us/cmpts_free.pdf