[sv-ac] Continuous assignments in checkers

Hi all,

Following our yesterday's discussion about continuous assignments of checker variables, I would like to address the question of free variable support in the RHS of a continuous assignment. The main concern was that currently we decided to disallow using free variables in the RHS of continuous assignments, and this can cause potential gap between simulation and formal verification.

It looks to me that the imposed restriction could be relaxed. It should be enough to require that continuously assigned variables whose right-hand side depends directly (i.e., without a cycle delay) on free variables may not be used in concurrent assertions. For example,

checker check(event clk);
default clocking @clk; endclocking
rand bit v;
bit a, b, c;
assign a = v; // Legal
a1: assert property (a == v); // Illegal - a is used directly in concurrent assertion
a2: assert #0 (a == v); // Legal
always @clk b <= a; // Legal
a3: assert property (b == $past(x)) ; // Legal
a4: assert property (b == $past(a)); //Illegal - a is used directly in concurrent assertion
assign c = b;
a5: assert property (c == $past(x)); // Legal
endchecker

I think it is a reasonable compromise.

Thanks,
Dmitry
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.