[sv-ac] RE: Call to vote: Due August 29 (resend with updated 3033)

Hi Anupam,

Mantis 3033 does not introduce anything new about assigning values to checker formal arguments. The same situation exists already in the LRM.

I suggest decoupling this issue from 3033. IMO, the most appropriate place to address it is Mantis 2093 "Checker construct should permit output arguments". To be on the safe side we can create a new Mantis especially for this issue in case 2093 is not completed.

About the issue itself: This restriction is not explicitly mentioned in the LRM but in most cases it is implied. It is possible to add the following restriction:

Checker formal (input) arguments shall not be assigned a value in a checker. However, a checker may constrain a set of possible values of its formal arguments using assumptions.

The second sentence describes the following situation:

checker check(a, clk);
                assume property(@clk a);
endchecker

In this case, in formal verification we essentially assign a value 1 to the (input) argument a, and this is a correct behavior regardless of the port direction. In simulation this assumption will fail if a is not 1. The open question here is what should the correct behavior in simulation be, if the corresponding actual argument is a free variable or contains a free variable as its subexpression.

Consider the following invocation:

checker outer(clk);
                rand bit v;
                check c1(v, clk);
endchecker

Should v be randomized in simulation in c1 or not? Different approaches may be considered:

1. Since checker instantiation has a substitution semantics, v should be randomized (even though a is an input port).

2. Allow formal port randomization by substitution only if it is an output argument, and the substitution semantics is used for output checker arguments. Currently, when checkers can have only input arguments it means that free variables may only randomized in the checker they are declared.

3. Do not allow formal port randomization by assumptions in any case. If wanted randomization should be performed explicitly in the inner checker:

checker check (output a, input clk);
                rand var type(a) x;
                assume property (@clk x);
                assign a = x;
endchecker

Though the last option is the most verbose, it is consistent with the rule that we don't randomize non-free variables in checkers.

Thanks,
Dmitry

From: Prabhakar, Anupam [mailto:anupam_prabhakar@mentor.com]
Sent: Tuesday, August 30, 2011 00:43
To: Korchemny, Dmitry; 'sv-ac@eda-stds.org'
Subject: RE: Call to vote: Due August 29 (resend with updated 3033)

Mantis 3033 ____ Yes __X__ No
http://www.eda-stds.org/mantis/view.php?id=3033

http://www.eda-stds.org/mantis/file_download.php?file_id=5366&type=bug

Can a checker port be driven from inside a checker ? There does not seem to be any text restricting this.
---------------------------------------------------------------------
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.