hello,
my qstn:
int count =0;
property a(int count)
@(posedge PCLK) (count ==0) s1 → s2 ##0 (1,count=1);
endproperty
property p2(int count);
@(posedge PCLK) (count ==1) s1 |-> s2 ##0 (1,count=2);
endproperty
can we not use global variables b/w properties.. how can we pass values between properties.
In reply to ramandeepk:
From my SVA Handbook 4th Edition
A local variable formal argument acts as a local variable of the sequence or property. It can be exported out only if direction inout or output (in sequence declarations only, and not in property declaration). An untyped formal argument cannot have a direction or a type; it can be treated as a local formal argument of direction input or output depending on how it is used within the sequence or property. An untyped formal argument can also be treated as a non-local formal argument if it is not assigned a value in the body of the sequence or property in which it is used. For example (Ch/2.7/type_m.sv)
bit clk, a, b, c;
default clocking cb_clk @ (posedge clk); endclocking
sequence q_local_formal_arguments2( local input int i=0,
untyped j, k,
local output bit t);
(i>10, j=i) ##1 (1, j=data, t=1'b1) ##1 k;
endsequence
property p_test_untype;
int x, z; // local variable
bit r; // local variable
(a, x=10) ##1 q_local_formal_arguments2( .i(x), .j(z), .k(a), .t(r)) ##1 x==z ##0 r;
endproperty : p_test_untype
ap_test_untype: assert property(p_test_untype);
I am providing 3 pages from my book here
There are more pages that describe all the rules, but I am not including it because it is complex. It’s in the book for completeness.
IMHO, I would not use the passing of inouts variables between sequences; It’s complex, and if your assertion really needs it, perhaps you should break it up into smaller pieces or use a different alternative. See my paper SVA Alternative for Complex Assertions Verification Horizons - March 2018 Issue | Verification Academy
It provides a SystemVerilog approach that uses all the features of SystemVerilog for specifying complex assertions.