Assertion to check signal activity occurred in past from current activity

SystemVerilog
, ,
1

Hi All,

Can someone help me to write an assertion for the below requirement?

signal A changes. After some clock counts, signal B changes. There might be a possibility that signal A can be changed while checking signal B activity.
So the check should be started from the point where signal A changes. (A & B both are single bit variable)

I tried the below way:
$rose(B) |-> ($past(A, count) == 1’b1)

To use the above code, the simulator says that count is a variable. It should be constant to use this approach.
Please help here.

Thanks,
Dhaval

2

In reply to Dhaval_Pandya:

signal A changes. After some clock counts, signal B changes. There might be a possibility that signal A can be changed while checking signal B activity.
So the check should be started from the point where signal A changes. (A & B both are single bit variable)

There is one ambiguity in your requirements: If I understand you correctly, you seem to want the following 2 requirements:

  1. $changed(a) |-> ##var_numb $rose(b); // $rose(a) ?
  2. $changed(a) and the $rose(b) is of concern for what reason?
  • Because it should not happen, or it is OK if it happens,
    If OK, then it can happen in the same cycle as the “a” or ##var_numb
    (I’ll show both (OK, Not OK) the code below)
  • Because if legal, then it would miss the assertion statement?

I tried the below way:
$rose(B) |-> ($past(A, count) == 1’b1)

QUESTION: Should assertions be written in a CAUSE then EFFECT or
EFFECT because of CAUSE style?
I prefer the CAUSE then EFFECT; no ‘detective’ work for created the cause?.
I created a library of sequences to use for dynamic delays, range delays, repeated, and range repeats. See


module m; 
  bit a, b, clk;
  int delay=3; 
// From the above library 
//----------------------------------------------------------------
// ******       DYNAMIC DELAY ##d1 **********
    // Implements     ##[d1] 
    // Application: sq_1 ##0 dynamic_delay(d1) ##0 sq_2;
    sequence dynamic_delay(count);
        int v;
      (count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);
    endsequence // dynamic_delay
  
// Cause then effect 
ap_ab: assert property(@ (posedge clk) $rose(a) |-> 
                       dynamic_delay(delay) ##0 b) or $rose(b);
ap_ab_no_rose: assert property(@ (posedge clk) $rose(a) |-> 
                       dynamic_delay(delay) ##0 b) and ! $rose(b);

// Effect because of cause 
sequence q_a2delay; 
   $rose(a) ##0 dynamic_delay(delay); 
endsequence 
// $rose(B) |-> ($past(A, count) == 1'b1)
// If rose(b) then in the same cycle the end point of (a ##delay) occurred 
ap_b_bcs_a: assert property(@(posedge clk) $rose(b) |-> q_a2delay.triggered or 
                                                        $rose(a)); // and ! $rose(a)?

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

Hi Ben,

Thanks for the quick response. Let me refresh my requirements here.

If signal A goes low, signal B should go LOW after the COUNT variable.

There might be a possibility that once signal A goes low, it can be HIGH in between the COUNT variable checking for signal B. (The above assertion should be disabled in this case)

I am planning to write a function call for assertion enable/disable bit. Can we write assertion for above requirement with function call ?

Thanks,
Dhaval

4

I tried the below approach but it didn’t help. (I think assertion is neither passed nor failed)

property cnt_check(X);
int count;
@(posedge clk) (fell(A), count=X) ##1 ((!A && count==0), count=count-1)[*1:] |-> $fell(B);
endproperty

A2B_count_chk:assert property(cnt_check(X) $display(“PASSED at %t”, $realtime);
else $display(“Assertion failed at %t”, $realtime);

Please help me to find the problem in the above code.

Thanks,
Dhaval

5

*In reply to Dhaval_Pandya:***Requirements:

  1. If signal A goes low, signal B should go LOW after the COUNT variable.
  2. If after signal A goes low, it goes HIGH during the COUNT then the assertion should be disabled.

**
I would use the sync_reject_on property operator; see below for more info. Thus,


ap_ab: assert property(@ (posedge clk) $fell(a) |-> 
            sync_reject_on($rose(a)) dynamic_delay(delay) ##0 $fell(b) );

Your assertion becomes vacuous when during the count a==1 because the antecedent is false.
((!A && count==0), count=count-1)[*1:$]


// Your assertion 
@(posedge clk) ($fell(A), count=X) ##1 ((!A && count==0), count=count-1)[*1:$] |-> $fell(B);

From my SVA book:3.10.9 accept_on, reject_on, sync_accept_on, reject_onsync_reject_on
This family of property operators provide an abort of the property being evaluated when the abort condition is true anytime during the evaluation of the property, and with an exit of vacuously true (for the accepts) or false (for the rejects) as the result of the property expression. This family of operators is not like the disable iff, which cannot be nested and asynchronously cancels the evaluation of the assertion with no contribution to the statistics. The accept_on/reject_on family of operators just terminates the property as an accept (true vacuously, with no contribution to the pass statistics) or reject (false, with contributions to the failed statistics). The abort operators can be nested (i.e., a lower property embedded into a higher level property can be aborted), and multiple aborts can exist in one property definition, whereas the disable iff must be at the top level of the assertion. If the abort condition is false, then the property expression continues to be evaluated until completion (i.e., to its end point, it is not aborted). These properties have the following forms:
accept_on ( expression_or_dist ) property_expr
reject_on ( expression_or_dist ) property_expr
sync_accept_on ( expression_or_dist ) property_expr
sync_reject_on ( expression_or_dist ) property_expr