Re: [sv-ac] Continuous assignments in checkers

Hi Dmitry,

I feel that this restriction is too complicated. I have no problem with
permitting random checker variables on the RHS of a continuous
assignment, but you get what you get. The simulation algorithm is
clearly defined, and everyone who is familiar with it, should be able to
see that assertion a1 is not going to behave as the author intended.
Of course, the tool is always free to print a warning message to try to
catch mistakes like this.

Why should a3 be legal and a4 be illegal? It seems to me that assertion
a4 should produce the desired result. The sampled value of variable a
will be used, and the current value of variable b will be used (except
that the assertion will be evaluated before the non-blocking assignment
takes place in the time step.

Tom

On 03/16/11 01:45, Korchemny, Dmitry wrote:
> 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* <http://www.mailscanner.info/>, and is
> believed to be clean.

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