RE: [sv-ac] Call to vote: Due June 20

Hi Ben,

Please, see my comments below.

Thanks,
Dmitry

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Wednesday, June 15, 2011 23:48
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org
Subject: Re: [sv-ac] Call to vote: Due June 20

Dmitry,
Questions on 3033:

* Arguments that cannot be sampled, such as events, sequences, and properties, are treated similarly to such arguments for sequences and properties (see 16.8): they are substituted directly for the formal argument when it is used in statements or expressions within the checker.
[Ben] In LRM 17.3 Why were the statements about sequences and properties deleted?
[Korchemny, Dmitry] This statement is not relevant anymore. It was included to the LRM to explain how the arguments that cannot be sampled are handled. Since checker argument sampling has been dropped in this proposal, there is no need to separately discuss this case. However, the next bullet ("If the checker is instantiated within another checker...") was dropped by mistake and I restored it. I also made several minor changes.

Nothing is mentioned about the handling of sequences and properties as arguments.
Consider the following example:
checker assert_window (
 logic test_expr, // Expression to be true in the window
 sequence start_event, // Window opens at the completion of the start_event
 sequence end_event, // Window closes at the completion of the end_event
 event clock = $inferred_clock,
 logic reset = $inferred_disable,
 string error_msg = "violation",
 coverage_level clevel = cover_all //This argument should be bound to an
  //elaboration time constant expression
);
  logic x, y;
  rand logic w;
  sequence IsThisLegal; // ??
       x ##1 start_event ##[2:10] w ##1 end_event;
  endsequence : IsThisLegal // ??

[Korchemny, Dmitry] In 17.2 it is written:
"All checker formal arguments are inputs and they are processed in a similar way as property formal arguments...", and in 17.3 we have:
"The mechanism for passing arguments to a checker is similar to the mechanism for passing arguments to a property (see 16.13)."

Editorial:

All forms of always procedures are allowed in checkers. A general purpose always procedure in checkers is equivalent to always_ff procedure and the same restrictions apply (see 9.2.2.4). All expressions in always and always_ff procedures except for the expressions in the event control are sampled (see 16.5.1
[Ben] I think you need a comma before the "and" , the "except", and "control" Does this read better?
[Korchemny, Dmitry] Fixed.

All forms of always procedures are allowed in checkers. A general purpose always procedure in checkers is equivalent to always_ff procedure, and the same restrictions apply (see 9.2.2.4). Except for the expressions in the event control, all expressions in always and always_ff procedures are sampled (see 16.5.1.

[Korchemny, Dmitry] Fixed.

[Ben] What about arguments of sequences or properties that are arguments of the checker. For example:

checker assert_window (
 logic test_expr, // Expression to be true in the window
 sequence start_event(logic x, y, clk), // Window opens at the completion of the start_event
 property P(logic x, y, int i);

[Korchemny, Dmitry] This is useful, but unfortunately illegal. I would be happy to have this capability in, but it is a serious enhancement in the language, and should be addressed separately.

[Ben] Editorial in 17.5 add a comma after always_ff procedure, as shown below.

But, I do have a question here: In this paragraph you explain the rationale for the changes, and why they are needed. But does that really belong IN the LRM? It seems to me that the LRM is more of a specification document, and does not necessarily need the rationalizations behind all the decisions. This rationalization belongs outside the p1800 doc, and more in the motivation and rationalization section. LRM has examples to further explain the points.
[Korchemny, Dmitry] I agree, there should be no justifications in the LRM. What is important is to stress the mere fact that checkers behave deterministically. I modified this sentence as follows: "Expression sampling in always and always_ff procedures makes checkers behave deterministically and not to depend on the order of process execution."
I also modified the example to show the module explicitly.

The assertion a1 passes in this case. Were the sampled values used in always_ff procedures, as it is done in modules, two scenarios could be possible
[Korchemny, Dmitry] Fixed.

17.7.1

* A checker variable may not be assigned in an initial procedure. For example:

bit v;

initial v = 1'b0; // Illegal

[Ben] How about adding something like:

* A checker variable may not be assigned in an initial procedure, but maybe initialized in its declaration. For example:

bit v, w=1'b1;

initial v = 1'b0; // Illegal

[Korchemny, Dmitry] Done.

Ben Cohen

On Wed, Jun 15, 2011 at 12:17 AM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:

-You have until 11.59 pm PDT, Wednesday, June 20, 2011 to respond

-An issue passes if there are zero NO votes and half of the eligible voters respond with a YES vote.

-If you vote NO on any issue, your vote must be accompanied by a reason. The issue will then be up for discussion during a future conference call.

As of the June 14, 2011 meeting, the eligible voters are:

Ashok Bhatt

Laurence Bisht

Eduard Cerny

Ben Cohen

Shaun Feng

Tapan Kapoor

Jacob Katz

Scott Little

Manisha Kulshrestha

Anupam Prabhakar

Samik Sengupta

Tom Thatcher

Mantis 3033 ____ Yes ____ No

http://www.eda-stds.org/mantis/view.php?id=3033
http://www.eda-stds.org/mantis/file_download.php?file_id=5152&type=bug

Mantis 3069 ____ Yes ____ No

http://www.eda-stds.org/mantis/view.php?id=3069
http://www.eda-stds.org/mantis/file_download.php?file_id=5142&type=bug

Below are the changes made in 3069:

- Replaced "global clocking declaration in effect" with "effective global clocking declaration"

- Fixed punctuation and spelling

- Changed
However, any of its instances in the elaborated design description shall contain at most one global clocking declaration. It shall be an error if there is more than one global clocking declaration in a given module, interface, checker or program instance in the elaborated design description.
To
However, any of its instances in the elaborated design description shall contain at most one global clocking declaration; it shall be an error otherwise.

- Changed
When global clocking is referenced in a sequence declaration, a property declaration, or as an actual argument to a named sequence instance, a named property instance, or a checker instance, the point of reference shall be considered after the application of the rewriting algorithm defined in F.4.1, which flattens properties and sequences, and substitutes actual arguments to sequence, property and checker instances for their corresponding formal arguments. As a result, when a property or a sequence declaration containing a reference to global clocking is instantiated in an assertion statement, the hierarchical lookup rules described above shall be applied from the place of the assertion statement appearance in the source description, not from the point of the sequence or the property declaration. Similarly, when global clocking is referenced in an actual argument of a checker instance, the lookup rules shall be applied after the substitution of the actual argument in place of the corresponding formal argument inside the checker body.
To
When global clocking is referenced in a sequence declaration, a property declaration, or as an actual argument to a named sequence instance, a named property instance, or a checker instance, the point of reference shall be considered after the application of the rewriting algorithm defined in F.4.1. As a result, when a property or a sequence declaration is instantiated in an assertion statement, the hierarchical lookup rules described above shall be applied from the place of the assertion statement appearance in the source description, not from the point of the sequence or the property declaration. Similarly, the lookup rules shall be applied after the substitution of the actual argument in place of the corresponding formal argument inside the checker body.

---------------------------------------------------------------------
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.
---------------------------------------------------------------------
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.