[b]In reply to puranik.sunil@tcs.com:[/b] My book has some 16 pages on local variables with examples.
Quote:
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 :)
Quote:
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 (K
eep It Simple Stupid).
Ben Cohen
http://www.systemverilog.us/
For training, consulting, services: contact http://cvcblr.com/home
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
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:
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- 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
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2