Question about the formal arguments of sequence and property

SystemVerilog
1

Hello,

I have a question on formal arguments of sequence and property - based on description given in SVA Assertions Handbook (Ben Cohen), the formal arguments of sequence and property can be local or non-local. Can someone explain what is the significance of “local” attribute here? What is the difference in local and non-local formal arguments of a sequence and a property?
(The SVA Assertions handbook (Ben Cohen) states that local variable formal arguments behave in the same way as local variables declared in an assertion_variable_declaration region of sequence or property. The book says terms local variable formal argument and local variable declared in assertion_variable_declaration are used interchangeably and mean same thing.)

Also formal arguments of sequence can be of the type input, output or inout but for the property they can be only input. Now if sequences are used in properties, what will be the use of output and inout arguments of sequences?

thanks and regards,
-sunil puranik

2

[b]In reply to puranik.sunil@tcs.com:[/b] My book has some 16 pages on local variables with examples.

I have a question on formal arguments of sequence and property - based on description given in SVA Assertions Handbook (Ben Cohen), the formal arguments of sequence and property can be local or non-local. Can someone explain what is the significance of “local” attribute here? What is the difference in local and non-local formal arguments of a sequence and a property?
(The SVA Assertions handbook (Ben Cohen) states that local variable formal arguments behave in the same way as local variables declared in an assertion_variable_declaration region of sequence or property. The book says terms local variable formal argument and local variable declared in assertion_variable_declaration are used interchangeably and mean same thing.)

What I wrote in the book is based on 1800’2017. In the Amazon review of my book I was criticized for defining things that did not work. The reality though is that NOT EVERYTHING THAT IS IN 1800’17 IS IMPLEMENTED!.
Per 1800’17 the following should work because in section 16.8.2 Local variable formal arguments in sequence declarations it states: a local variable formal argument behaves in the same way as a local variable declared in an assertion_variable_declaration.
Thus, the following should work if the tool implements this feature:


     sequence  q_x(local int v); 
      ($rose(a), v=bus1) ##3 bus1=v+1'b1;
     endsequence 
     
    ap: assert property(a |-> q_x);  

    property p_x(local int v); 
      ($rose(a), v=bus1) |-> ##3 bus1=v+1'b1;
    endproperty 
    ap: assert property(p_x);

Unfortunately, it seems that tools have not implemented this feature. I get something like near “=”: syntax error, unexpected ‘=’, expecting ++ or --.
In your reviews, please do not blame the messenger :)

Also formal arguments of sequence can be of the type input, output or inout but for the property they can be only input. Now if sequences are used in properties, what will be the use of output and inout arguments of sequences?

I provided the following example in the book


sequence q_test ( // ch2/2.7/auto_var.sv 
        local inout int lv_count);
         (a, lv_count+= 1); //
    endsequence : q_test
       
      property p_test_OK;
      int v_c;
      (1, v_c=0) ##0 q_test(v_c) //  v_c is uninitialized, value read in q_test
      endproperty : p_test_OK
      ap: assert property(p_test_OK);

Curiously, the above example compiles and elaborates, but the example above fails.
My guess is that not all features of what is in 1800 are implemented. They could be selectively implemented.
Throughout all of my applications and examples and responses to users’ questions, I never felt a need to use those special variable features (e.g., local, inout). I try to KISS (Keep It Simple Stupid).

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
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
3

HI Ben,
thanks for immediate reply.
I am still not clear about the use of local formal arguments in properties and sequences. For example, in sequence q_x above, if we make the property non local what difference would it make? On Page no 63, section 2.7 of your SVA assertions handbook, 4th edition, it is said that non local argument is by default of direction input and cannot be written into. Is this true for both sequence and property? Does this mean, in a sequence, if we declare v as non local (remove local attribute), we will not be able to write to it even if its direction is output?
Also in property p_x example you have given above, you are assigning to argument v (statement v = bus1). However, according to the book, formal arguments direction can be only input for a property (for a sequence it could be output, input or inout). Can you please explain.

Also your book says that for untyped formal arguments can be treated as local local formal argument of direction input or output depending upon how it is used in sequence or property. Is this true for property also where formal arguments are always supposed to be of type input?

thanks and regargs,
-sunil puranik

4

In reply to puranik.sunil@tcs.com:
I rarely used local variables being passed from a property to a sequence and back to the property. Below is an example that does that to see what the compiler and simulation does. I’ll admit that often in learning design languages (VHDL, PSL, SV, SVA)and when the LRM is unclear, I often refer to simulating a model (hoping that the vendor understands the issue).


// This is a straight forward model without passing local variables around
property p_eq; 
      int v_c;
      @ (posedge clk) $rose(a) |-> (1, v_c=0) ##1  (1, v_c=v_c+1'b1) ##1 v_c==1; 
endproperty   
ap_eq: assert property(@ (posedge clk) p_eq );

// In this model, a property local variable (v_c) is passed to a sequence, 
// it is modified there and is then passed back to the property 
// where v_c is compared to a value 
sequence q_test ( // ch2/2.7/auto_var.sv
   // inout int lv_count); // syntax error, unexpected inout, expecting ')'
   local inout int lv_count);
   (1, lv_count+= 1); //
endsequence : q_test
       
property p_test_OK;
  int v_c;
  $rose(a) |-> (1, v_c=0) ##1 q_test(v_c) ##1 v_c==1; //  
endproperty : p_test_OK
ap_test_OK: assert property(p_test_OK);

1800’2017 16.8.2 Local variable formal arguments in sequence declarations
A formal argument of a named sequence may be designated as a local variable argument by specifying the keyword local in the port item, followed optionally by one of the directions input, inout, or output.
Thus, without the identifier local the actual argument being passed is by value.
However, with the word local that is being passed is the actual local variable of the calling party. In the example above, in the sequence q_test the actual argument passed to lv_count is a local variable from the calling party. It is not just its value. This explains why


 ( inout int lv_count); // syntax error, unexpected inout, expecting ')'
// is in error because it is an inout.  Without the "local" identifier, 
// only the value is v=passed, but then it cannot act like the calling variable;  
// that is illegal.  
// With the "local", the sequence formal argument acts like a local variable of a sequence 
 local inout int lv_count); // IS LEGAL

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
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: