[sv-bc] Continuous assignments and checker variable sampling

Hi all,

I am copying SV-BC in case some SV-BC people want to take part in the discussion. The below description has not been discussed yet in SV-AC.

It looks like we have a serious problem in the definition of continuous assignments of checker variables. Consider the following example:

checker check (bit a, event clk);
                default clocking @clk; endclocking
                rand bit v;
                bit w, u;
                m1: assume property ($onehot0({a, v});
                assign w = !v;
                assign u = !a;
                a1: assert property ($onehot0({a, !w});
                a2: assert property ($onehot0({!u, v});
endchecker : check

It is natural to expect that assertions a1 and a2 always pass. The question is whether checker variables w and u are sampled in the Preponed region in concurrent assertions. If they are, assertion a1 will fail. If they are not, assertion a2 will fail. This means that the RHS of the continuous assignment should be sampled (i.e., regular variables are sampled in the Preponed region, and the current value of free variables is used), and that the continuously assigned checker variables should not be sampled (in the Preponed region). This also means that the continuous assignment should be performed in the Observed region, as was suggested in the original version of the checker proposal (1900). This, however, requires a refinement of the simulation semantics definition of the Observed region by imposing some evaluation order in it. Some ordering implicitly exists in the LRM at least since 2005. E.g., if a sequence method is used in another sequence, the former sequence should be evaluated before the latter one. LRM 2009 adds a new restriction that free checker variables should be evaluated before the assertions where they are used. Thus in the above example, the assumption m1 must be evaluated before assertions a1 and a2. Introduction of the continuous assignments requires imposing a stricter ordering: if variable x depends on variable y then y should be evaluated before x. For the above example it means that m1 is evaluated first, then the assignments in any order, and then the assertions in any order.

There exists a strong objection against imposing any evaluation ordering, but what is an alternative?

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.