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

Dmitry,
Thanks for the comments. Question:

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

[Ben2] LRM states:

checker_port_item ::=

  { attribute_instance } property_formal_type port_identifier
{variable_dimension}

      [ = property_actual_arg ]

property_formal_type ::= sequence_formal_type | property

But the use of sequence seems limited to the .triggered, and I fail to see
the use of a formal argument being a property. Let me explain thru an
example:
checker C(logic a, b,
                   event e,
                   sequence s;
                    property p);
  ap_legal_but_will_it_work: assert property(@ (e)
           a ##1 s |-> p);
endchecker : C
module m;
  logic a, b, c, e, f, g clk;
  sequence q; e ##2 f; endsequence : q
  property pm;
    a ##1 b |-> g;
  endproperty :pm
   C c1(a, b, posedge clk, q, pm);
endmodule : m

What would be the equivalent of the checker instance c1 in module m?
I am passing the sequence q, but in the checker, q does not see the module
variables e, f. Or does it?
Same question for the checker formal "p". The actual is pm, but does the
checker see the module variables of pm (i.e., the a, b, and g)?
I understood that [LRM] I*t shall be illegal to reference a checker variable
using its hierarchical name in assignments. *Also, in that case, the module
variables are not directly visible.
Thus, my assertion in the checker is useless, and does nothing.
ap_legal_but_will_it_work: assert property(@ (e)
           a ##1 s |-> p);
Am I missing something here?
Unless I can pass arguments to the sequence or property of the checker port
list, I don't understand how a simulator can do the job.
Thanks,
Ben Cohen

On Tue, Jul 5, 2011 at 6:03 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

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