How to block error message from assertion

SystemVerilog
,
1

Hi all,
I want to check clock frequency by asssertion, but there is a problem, the ‘valid’ signal is not sinchronized to the clock, so when it de-assert, the assertion already in the middle of checking the expression. In this case I will get an error message at time that the ‘valid’ is 0.
Is there any option to mask the error message in case that ‘valid’ deassert or to check tha ‘valid’ value before the second waiting to the clock rising edge?

Original code:
property p_clk_freq;
time rising_time;
@(posedge clk) disable iff (!freq_valid)
(1, rising_time=$time) |=> @(posedge clk) ($abs(int’(($time-rising_time))-int’((period*1.0ps)))<= TOLERANCE);
endproperty

Desired code:
property p_clk_freq;
time rising_time;
@(posedge clk) disable iff (!freq_valid)
(1, rising_time=$time) |=> disable iff (!freq_valid) @(posedge clk) ($abs(int’(($time-rising_time))-int’((period*1.0ps)))<= TOLERANCE);
endproperty

Thank you

2

In reply to Yehu:
Why do you say In this case I will get an error message at time that the ‘valid’ is 0.?
The disable iff is asynchronous.
1800’16.12 Declaring properties
The expression of the disable iff is called the disable condition. The disable iff clause allows preemptive resets to be specified. For an evaluation of the property_spec, there is an evaluation of the underlying property_expr. If the disable condition is true at anytime between the start of the attempt in the Observed region, inclusive, and the end of the evaluation attempt, inclusive, then the overall evaluation of the property results in disabled. A property has disabled evaluation if it was preempted due to a disable iff condition. A disabled evaluation of a property does not result in success or failure.
Otherwise, the evaluation of the property_spec is the same as that of the property_expr. The disable condition is tested independently for different evaluation attempts of the property_spec. The values of variables used in the disable condition are those in the current simulation cycle, i.e., not sampled. The expression may contain a reference to an end point of a sequence by using the method triggered of that sequence. The disable conditions shall not contain any reference to local variables or the sequence method matched. If a sampled value function other than $sampled is used in the disable condition, the sampling
clock shall be explicitly specified in its actual argument list as described in 16.9.3. Nesting of disable iff clauses, explicitly or through property instantiations, is not allowed

Another option is explained in 1800’2017 16.12.14 Abort properties
A property is an abort if it has one of 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

For an evaluation of accept_on (expression_or_dist) property_expr and of
sync_accept_on (expression_or_dist) property_expr, there is an evaluation of the underlying
property_expr. If during the evaluation, the abort condition becomes true, then the overall evaluation of the property results in true. Otherwise, the overall evaluation of the property is equal to the evaluation of the property_expr.


   //Desired code:
     property p_clk_freq2;
        realtime rising_time;
        @(posedge clk) disable iff (!freq_valid)
        (1, rising_time=$realtime) |=> accept_on (!freq_valid) @(posedge clk) 
              ($abs(int'(($realtime-rising_time))-int'((period*1.0ps)))<= TOLERANCE);
    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
  4. Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
  5. FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
3

In reply to ben@SystemVerilog.us:
One more note on making the disable iffsynchronous:
From my SVA book:
Sampled value Function: If a sampled value function other than $sampled is used in the disable condition, the sampling clock must be explicitly specified in its actual argument list. Thus, the following is legal:


        apP1: assert property ( // /ch3/3.8/reset2.sv
             disable iff  ($rose(reset, @(posedge clk)))
•	          @ (posedge clk) req |=> ack);    // disable sampled at @ (posedge clk1) 
        apP2: assert property ( 
            disable iff  ( $sampled(reset))
•	          @ (posedge clk) req |=> ack);  
        property pXY(x,y, reset);  // active hi reset 
          int v;       
          disable iff (reset)   
            (x, v=0) |=> y && v==data;
        endproperty : pXY
        apXY_sampled: assert property (@(posedge clk) 
                pXY(req, ack, $sampled(reset)));
     // disable sampled at @ (posedge clk)

**Nesting:**Nesting of disable iff clauses, explicitly or through property instantiations, is not allowed. The disabling condition must only appear at the top level of an assertion. It cannot be nested; this is unlike the accept_on, reject_on, sync_accept_on, sync_reject_on operators that allow nesting (see 3.9.2.14). The following nesting of disable iff example is illegal:

             assert property ( @ (posedge clk) disable iff (cancel) 	                              
       pXY(req, ack, reset));   // pXY has a disable iff

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
  4. Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
  5. FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
4

In reply to ben@SystemVerilog.us:

Hi,
Thank you for your reply.
One more question:
If I understand correctly, accept_on means that if the expression that comes after it is true, the propery_expression will be sampled. So in my case I have to use reject_on(!freq_valid), Or accept_on (freq_valid).

Is it true?

Thank you
Yehudit

5

In reply to Yehu:

In reply to ben@SystemVerilog.us:
If I understand correctly, accept_on means that if the expression that comes after it is true, the propery_expression will be sampled. So in my case I have to use reject_on(!freq_valid), Or accept_on (freq_valid).

There are 2 variations of the accept, the asynchronous and the synchronous.
accept_on ( expression_or_dist ) property_expr // asynchronous, whenever it occurs
sync_accept_on ( expression_or_dist ) property_expr // sampled
Thus, whenever the !freq_valid==1 the assertion is true.
See this simple test


    initial forever #10 clk=!clk;   // for the assertion  
    initial forever #3 clk2=!clk2; // Changes the "a" at posedge(clk2) 
 ap_accept: assert property( 
      1 |=>  accept_on(a) 0
    ) $display("%t a= %d  pass", $realtime, $sampled(a)); 
      else $display("%t a= %d  fail", $realtime, $sampled(a)); 
/*  30 a= 1  pass
#                   50 a= 0  fail
#                   70 a= 1  pass */
6

In reply to ben@SystemVerilog.us:

In reply to Yehu:
Why do you say In this case I will get an error message at time that the ‘valid’ is 0.?
The disable iff is asynchronous.
1800’16.12 Declaring properties
The expression of the disable iff is called the disable condition. The disable iff clause allows preemptive resets to be specified. For an evaluation of the property_spec, there is an evaluation of the underlying property_expr. If the disable condition is true at anytime between the start of the attempt in the Observed region, inclusive, and the end of the evaluation attempt, inclusive, then the overall evaluation of the property results in disabled. A property has disabled evaluation if it was preempted due to a disable iff condition. A disabled evaluation of a property does not result in success or failure.
Otherwise, the evaluation of the property_spec is the same as that of the property_expr. The disable condition is tested independently for different evaluation attempts of the property_spec. The values of variables used in the disable condition are those in the current simulation cycle, i.e., not sampled. The expression may contain a reference to an end point of a sequence by using the method triggered of that sequence. The disable conditions shall not contain any reference to local variables or the sequence method matched. If a sampled value function other than $sampled is used in the disable condition, the sampling
clock shall be explicitly specified in its actual argument list as described in 16.9.3. Nesting of disable iff clauses, explicitly or through property instantiations, is not allowed

Another option is explained in 1800’2017 16.12.14 Abort properties
A property is an abort if it has one of 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

For an evaluation of accept_on (expression_or_dist) property_expr and of
sync_accept_on (expression_or_dist) property_expr, there is an evaluation of the underlying
property_expr. If during the evaluation, the abort condition becomes true, then the overall evaluation of the property results in true. Otherwise, the overall evaluation of the property is equal to the evaluation of the property_expr.


//Desired code:
property p_clk_freq2;
realtime rising_time;
@(posedge clk) disable iff (!freq_valid)
(1, rising_time=$realtime) |=> accept_on (!freq_valid) @(posedge clk) 
($abs(int'(($realtime-rising_time))-int'((period*1.0ps)))<= TOLERANCE);
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
    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
  4. Understanding the SVA Engine,
    https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
  5. https://verificationacademy.com/forums/announcements/free-book-component-design-example-…-step-step-process-using-vhdl-uart-vehicle

Hi Ben,
is that extra @(posedge clk) needed on the RHS of non overlapping implication operator? I believe it adds one more clock cycle to the calculation.

7

In reply to MSB:

That extra @(posedge clk) is NOT needed on the RHS of non overlapping implication operator. It is not needed because the initial clocking event (i.e., the one in the @(posedge clk) disable iff (!freqed_valid)) flows through to the consequent.

And NO, that extra @(posedge clk) does not adds one more clock cycle to the calculation. That extra clocking event is typically used in multiclocking. Fro example:


ap0: assert property(@(posedge clk1) $rose(a) |-> @(posedge clk2) b);

If you use the same clocking, it is considered a multiclocking where the 2nd clocking event is in sync with the first.

BTW, I had it because I copied your assertion and was concentrated on your initial problem of block error message and not the assertion itself. Actually, you do not needed and it is confusing if you do add it. Remeber, the clock flows from the antecedent to the consequent.
SVA has specific rules on clock flow and sequences. The LRM explains them, and I demonstrate them in my SVA BOOK (4.3 Clocked Sequences, Properties, And Multiclocking).
Ben SystemVerilog.us

8

In reply to ben@SystemVerilog.us:

Thanks, Ben.