Checking clock period using system verilog assertion

In reply to ben@SystemVerilog.us:

ok thanks ,it was very helpful

In reply to SAKET@ KUMAR:

How can we check whether Ton and Toff of the clock are as desired (using SVA)?

In reply to perumallatarun:

See vhttps://verificationacademy.com/forums/systemverilog/checking-clock-using-sva

In reply to ben@SystemVerilog.us:
Hi All,
When I run the above code in VCS I am getting the following error please let me know any switches in the command line to be used. Or if this should be run using specific version of vcs(I am using version 2013 of vcs).

Error-[SVA-ITRHS] Invalid type in local variable assign
clock_generate_assert.sv, 6
clock_assert, “$realtime”
Expressions involving real, realtime, string, event and dynamic
SystemVerilog types including virtual interface references are not allowed
in local variable assignments in properties and sequences.

Regards,
Rajesh.B

In reply to rajeshsois:

This forum is not for tool issues. You will need to contact your vendor directly for support.

In reply to rajeshsois:

In reply to ben@SystemVerilog.us:
When I run the above code in VCS I am getting the following error please let me know any switches in the command line to be used. Or if this should be run using specific version of vcs(I am using version 2013 of vcs).

Error-[SVA-ITRHS] Invalid type in local variable assign
clock_generate_assert.sv, 6                            
clock_assert, "$realtime"

Expressions involving real, realtime, string, event and dynamic
SystemVerilog types including virtual interface references are not allowed
in local variable assignments in properties and sequences.

As mentioned, this forum does not address tools. However, it DOES address language issues. Referring to 1800: 16.6 Boolean expressions


/* Assertions that perform checks based on time values should capture these values in the same context. It is not recommended to capture time outside of the assertion. Time should be captured within the assertion using local variables. The following example illustrates how a problem may arise when capturing time in different contexts. In property p1, a time value, t, is captured in a procedural context based on the current value of count. Within the assertion, a comparison is made between the time value t and the time value returned by $realtime in the assertion context based on the sampled value of count. In both contexts,
$realtime returns the current time value. As a result, the comparison between values of time captured in the different contexts yields an inconsistent result. The inconsistency results in the computation for p1 checking the amount of time that elapses between 8 periods of clk instead of the intended 7. In property p2, both time values are captured within the assertion context. This strategy yields a consistent result. */
bit count[2:0];
realtime t;
initial count = 0;
always @(posedge clk) begin
  if (count == 0) t = $realtime; //capture t in a procedural context
  count++;
end
property p1;
  @(posedge clk)
  count == 7 |-> $realtime – t < 50.5;
endproperty
property p2;
  realtime l_t;
  @(posedge clk)
  (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |->
                  $realtime – l_t < 50.5;
endproperty

Thus, realtime and $realtime can be used in assertions. If a tool doe snot abide by those rules, you need to contact the vendor, and quote him that section and example of the LRM.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • 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 0-9705394-2-8
  • 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

Hi I know this is an old thread, but I’m quite interested in the OP’s assertion code as I’m trying to write clock assertions as well. I have two questions:

  1. In the property, the OP has written this:
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));

What is the '1 at the beginning of the statement for? What does it achieve?

  1. Let’s say I want to pull out the value of $realtime-current_time into an error message if this property catches a failure. Is there a way I can pull out the value of a variable inside a property? If not, what are my options?

Thanks!

In reply to silverace99:

Hi I know this is an old thread, but I’m quite interested in the OP’s assertion code as I’m trying to write clock assertions as well. I have two questions:

  1. In the property, the OP has written this:
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));

What is the '1 at the beginning of the statement for? What does it achieve?

The 1’b1 (a more typical application here) makes the antecedent true, and thus variable in the sequence match item is updated. You can replace the 1’b1 with a variable (e.g., k), but if that variable evaluates to zero, the property is vacuous.

  1. Let’s say I want to pull out the value of $realtime-current_time into an error message if this property catches a failure. Is there a way I can pull out the value of a variable inside a property? If not, what are my options?

Two solutions: Edit code - EDA Playground


module M;
  bit clk; 
  realtime t1, clk_period=20.0;
  initial forever #11 clk=!clk; 

  property p2;
   realtime current_time;
   @(posedge clk)
    ('1,current_time=$realtime) |=>
    (clk_period==$realtime-current_time);
  endproperty
  ap2: assert property(p2) else 
     begin 
       $display ("error"); // local variable is not accessible here ******!!!
     end  
    
 
    function automatic bit check_period(realtime now_time); 
      if ($realtime-now_time != clk_period) begin 
        t1=$realtime-now_time; // <<<<module variable update here
        return 0;
      end 
      else return 1'b1;   
    endfunction : check_period
    
   property p3;
     realtime current_time;
     bit pass;
     @(posedge clk)
      ('1,current_time=$realtime) |=>
     (1, pass=check_period(current_time));
  endproperty
    ap3: assert property(p3);  
 endmodule 

Another option is to use tasks and do whatever you want. See my recently published paper

Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.

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


In reply to ben@SystemVerilog.us:

I see. so by pulling all the variables into a function, you’ve moved the variable scope up to a level an error message can access. Very cool. Thanks Ben!

In reply to silverace99:

Should be
(1, pass=check_period(current_time))##0 pass;
This makes the assertion pass or fail.

In reply to raghav kumar:

Hi, can you tell me that why '1 is used in ('1,current_time=$realtime)?
Also whats the difference if we write 1 instead of '1 or if we write any other number 2,3 etc.

In reply to akashsoni29:

Actually, it should be 1’b1 as that is the standard definition of “true”.
Of course, any number other than zero would work.
I had a typo when I wrote '1,apologies.
Better stick to a standard.
Ben

In reply to ben@SystemVerilog.us:

FYI: '1 used in a self-determined context is the same as 1’b1.

In reply to ben@SystemVerilog.us:

Hi Ben,

Ive been following your book on assertions(SystemVerilog Assertions Handbook, 4th Edition) and on page 331 it says:

property period_chk;
realtime current_time, deltat;// deltat used for debug, as a temp
('1,current_time = $time) ##1 (1, deltat=current_time) ##0 deltat == 10ns;
endproperty ap_time:

assert property(@(posedge clk) period_chk);

should there be a difference in the underlined portion.

regards
Vijay

In reply to vijay kumar uba:

I don’t know where that property came from. The correct answer is
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
Ben

In reply to ben@SystemVerilog.us:

Hi Ben
What is difference when declaring clk_period to be real type instead of realtime type?

In reply to peter:

There is no difference between the keywords real and realtime. Very early versions of Verilog did not specify the precision of “whole” datatypes like time, integer, realtime, real. Implementations could choose different precisions to get the best performance in different situations. Later versions have now fixed the precision so there is no longer any difference.

In reply to dave_59:
From a “readability” standpoint, it seems to make more sense to type a variable that deals with “time” as realtime instead of real. But is there an issue by declaring a variable real and then comparing that with a value obtained from $realtime?
1800’2017: 5.8 Time literals
Time is written in integer or fixed-point format, followed without a space by a time unit (fs ps ns us ms s). For example: 2.1ns 40ps The time literal is interpreted as a realtime value scaled to the current time unit and rounded to the current time precision.

This, if I do


timeunit 1ns;  timeprecision 100ps;
initial begin  
  real vr; 
  realtime vt;
  vr=2.0; // What if I wrote vr=$realtime? Any difference 
  vt=$realtime;
  #12;
  if($realtime == vr*1ns) action(); 
   // DO I need the *1ns? 
  if($realtime == vt) action(); 
   // Here you definitely don't need the *1ns because 
   // VT was declared as realtime 

Question: Are my statements above correct?
Somehow, that makes more sense to me.

Hi Ben,

For the checking the clock period, can you please check if this way of writing is correct ?

I am using a var to send to the the property which can be any freq (XMHz). So if its 10MHz freq, then the clk period is 100ns, so i will ensure that the clk is high for 50ns and low for next 50ns giving me a 100ns clk period.

timeunit 1ns;
property pclk (int freq);
int lv;
lv = 1.0/freq;

ref_clk[*lv] |-> ! ref_clk[*lv];
endproperty

assert property (@(posedge clk) pclk(10);

In “sig[*n]”, n has to be a static number.

So, your code is non-complilable.
Also, if freq==10, then in
ref_clk[*lv] |-> ! ref_clk[*lv]; you get
ref_clk[*0.1] |-> ! ref_clk[*0.1];
// which is nonsense, sorry!
Ben