Checking clock period using system verilog assertion

SystemVerilog
,
1

i have been trying to assert the clock period of clock having frequency 340 MHz using following systemverilog code

realtime clk_period =1000.0/340.0ns;
property T_clk(int clk_period);
time current_time;
disable iff(!RESET_N || !ENABLE)
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
endproperty

assert_period:assert property (@(posedge clk)T_clk(clk_period))
else
$warning("%t TB_INFO : clk not correct",$realtime);

assertion gets active with posedge of clk but after next clk edge it shows failed instead of finish.
assertion is failing
what may be the problem and possible solution

2

The issue here is that the formal argument of the property is of type “int”, yet you’re passing as actual a realtime. Per 1800
“integer_atom_type ::= byte | shortint | int | longint | integer | time
non_integer_type ::= shortreal | real | realtime”
The following code worked OK

module m2b; 
	time clk_period =20.0/1.0ns;
	bit clk, RESET_N, ENABLE;
	property T_clk(int clk_period);
		realtime current_time;
		// disable iff(!RESET_N || !ENABLE)
		(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
    endproperty
 
    assert_period:assert property (@(posedge clk)T_clk(clk_period))
	   $display("%t TB_INFO : clk  correct",$realtime); 
       else
	   $warning("%t TB_INFO : clk not correct",$realtime);
    initial forever #10 clk=!clk; 
    initial begin 
	  $display("START");
	  repeat(10) @(posedge clk); 
	  $finish; 
    end
endmodule : m2b
3

In reply to ben@SystemVerilog.us:

Thanks it was helpful to certain extent
I m not able to keep formal argument of property to real data type

here
time clk_period = 20.0/1.0ns that means clk_period is effectively 20
but how to find for 340 MHz.
time clk_period = 1000.0/340.0ns that means clk period is effectively 2.94…
how to write code for this frequency.

4

In reply to raghav kumar:

The issue is that you’re dealing with real numbers, thus the “==” is not going to work because of resolution.
You’ll need to specify a range of acceptable accuracy. Below is code that worked, but you need to set the acceptable ranges and timescales, using the timeunit and timeprecision

module m2b;
         timeunit 1ns;     timeprecision 100ps;  
	realtime clk_period =1000.0/340.0ns;   // =2.941176470588235
	bit clk, RESET_N, ENABLE;
  property T_clk(real clk_period);
		time current_time;
		// disable iff(!RESET_N || !ENABLE)
		(('1,current_time=$realtime) |=>
         (clk_period <= $realtime-(current_time-0.001ns))  ||
         (clk_period >= $realtime-(current_time + 0.001ns))); 
endproperty
 
assert_period:assert property (@(posedge clk)T_clk(clk_period))
	$display("%t TB_INFO : clk  correct",$realtime); 
else
	$warning("%t TB_INFO : clk not correct",$realtime);
initial forever #1.470 clk=!clk; 
initial begin 
	$display("START");
	repeat(10) @(posedge clk); 
			// $display("%t %t TB_INFO : clk  correct",$realtime, $realtime);
	$finish; 
end
   
endmodule : m2b

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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
5

In reply to ben@SystemVerilog.us:

thank u it was great help ,now the code is working
replacing || with && and current_time and clk_period should have same data type. :)

6

In reply to raghav kumar:

I have a question. I’m still learning SVA, and I have not seen the following syntax used in the above example.
Could you tell me what the antecedent part ( (('1,current_time=$realtime) ) means? Thank you.

(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));

7

In reply to jaecho@broadcom:

Could you tell me what the antecedent part ( (('1,current_time=$realtime) ) means?
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));

The ('1,current_time=$realtime) is called a sequence_match_item

sequence_expr ::=  // one of the possibilities is   
( sequence_expr {, sequence_match_item }) [ sequence_abbrev ]

sequence_match_item ::=
    operator_assignment
  | inc_or_dec_expression
  | subroutine_call

sequence_abbrev ::= consecutive_repetition
consecutive_repetition ::=
  [* const_or_range_expression ]
  | [*]
  | [+]

In this case, ('1,current_time=$realtime) the '1 is a sequence expression, which means that at every attempt, it will succeed. sequence_match_item are typically used in things like


property p; // if wr, data -> mem, check data is properly written after 4 cycles 
  int v_data, v_addr;   // this is a slow memory, or it goes through other paths. 
  (wr, v_data=data, v_addr=addr) |-> ##4 mem[v_addr]==mem_data;
endproperty

Ben Cohen SystemVerilog.us

8

In reply to ben@SystemVerilog.us:

Thank you for your answer. I could not look for this in LRM, since I did not know what this is called (sequenc_match_item). I do see it now.
BTW, I have your book (SystemVerilog Assertions Handbook) and just getting started with it.

9

In reply to jaecho@broadcom:

BTW, I have your book (SystemVerilog Assertions Handbook) and just getting started with it.

I hope you find the book useful for your projects. Make sure you understand in chapter 1 the section on attempts and threads. Also make sure you understand the needs for the first_match operator. Understanding those concepts can save lots of time. The dictionary of examples is also very useful as it reinforces the uses of the various constructs.
Ben SystemVerilog.us

10

In reply to ben@SystemVerilog.us:

I am new to system verilog assertions , i have read in the LRM that real data type is not allowed to be passed to property but in the above example of clock
checker it is being passed .

can you help me on this

11

In reply to SAKET@ KUMAR:

You CAN use real in expressions that result in a Boolean. For example

property preal; 
    	real v; 
    	(a, v=3.14) |=> v> 4.0; 
    endproperty 
    ap_real: assert property(@(posedge clk) preal  );

You cannot use real in clock delays or repeat time.


// ILLEGAL
    a ##1.2 b
12

In reply to ben@SystemVerilog.us:

ok thanks ,it was very helpful

13

In reply to SAKET@ KUMAR:

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

14

In reply to perumallatarun:

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

15

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

16

In reply to rajeshsois:

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

17

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
18

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!

19

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

20

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!