Hi Ben,
I might have misunderstood your question. Your example is legal since the checker is essentially inlined at the point of its instantiation, and therefore the checker can see the module variables. The following is illegal:
checker check (sequence s, property p, untyped x, event clk);
assert property (@clk s(x) |-> p);
endchecker
...
logic a, b, clk;
sequence seq(v); v[*2]; endsequence
property prop; always b; endproperty
check mycheck(seq, prop, a, posedge clk);
Regards,
Dmitry
From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Wednesday, July 06, 2011 07:59
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org
Subject: 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] It 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<mailto:dmitry.korchemny@intel.com>> wrote:
Hi Ben,
Please, see my comments below.
Thanks,
Dmitry
From: ben cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>]
Sent: Wednesday, June 15, 2011 23:48
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org<mailto: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. --------------------------------------------------------------------- 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.Received on Wed Jul 6 06:17:29 2011
This archive was generated by hypermail 2.1.8 : Wed Jul 06 2011 - 06:17:36 PDT