Re: [sv-ac] Can checker assign value to variable outside its boundary?

Hello Everyone,

I haven't found that

17.2 says:
"Variables used in a checker that are neither formal arguments to the
checker nor internal variables of the checker are resolved according to
the scoping rules from the scope in which the checker is declared."

 From this, I infer that a checker could reference a variable that would
be visible to it using normal scoping rules. For example, if the
checker is defined within another module or checker, any variable
defined in the containing module or checker would be visible to the
checker. Another case would be if a variable is defined in the
compilation unit where the checker is defined. In that case the
variable would also be visible to the checker.

But can the checker assign to it. Our working assumption was always
that it couldn't, but I can't find the text in the LRM that says this.

17.2 does say that the checker body may contain checker variable
declarations and assignments. The list at the bottom of page 422
doesn't contain any other variable types, so we might be able to argue
that assignments to other types of variables are illegal.

Also, 17.5 says that

"An always procedure in a checker body may contain deferred and
concurrent assertions, nonblocking variable assignments (see 17.7.1) and
a procedural timing control statement using an event control. All other
statements shall not appear inside an always procedure."

But this says "variable assignments", not "checker variable
assignments". However, I think that the text in 17.2 rules out
assignments to non-checker variables.

In the case of a checker defined within a checker, this would still
allow for the enclosing checker to define a checker variable, and for
the checker defined within it to assign to it, as long as it doesn't
break the single assignment rule

So I don't think that we can drop 2858 so easily. Did I miss something?

Tom

On 04/23/10 14:27, ben cohen wrote:
> *Several points addressed here, and possibly some more mantises. *
> *1) _checker declaration within a module_*
> *From my experience with checkers from our DvCon paper (
> see **http://systemverilog.us/DvCon2010/** for paper, slides, and code)
> I learned that that *
> *from a "practical standpoint", a checker declaration inside a module,
> or a module declaration inside a module is not supported by vendors. *
> *The LRM allows the declaration of modules within modules, or checker
> within a module. *
> *One of the things I was discussing is something like the model below,
> and in module */*m_with_checkers_declarations */*the question is the *
> *access (read/write) of module variable "a". This
> is reference to **17.2 "Variables used in a checker that are neither
> formal arguments to the checker nor internal variables of the*
> *checker are resolved according to the scoping rules from the scope in
> which the checker is declared." *
> *
> *
> *module m_with_checkers_declarations;*
> * logic, a, b, c, d. clk;*
> * checker chk_not_supported_by_vendors(logic clk, x, y);*
> * logic w;*
> * ap_xy: assert property(@ (posedge clk) x|-> y);*
> * always @ (posedge clk) w <= a; // Supported??? *
> * ..*
> * endchecker :chk_not_supported_by_vendors*
> *
> *
> * **chk_not_supported_by_vendors chk_not_supported_by_vendors_1(clk, a, b);*
> *endmodule : m_with_checkers_declarations*
> *
> *
> *My questions to this committee are: *
> *a) what does this mean? **17.2 "Variables used in a checker that are
> neither formal arguments to the checker nor internal variables of the*
> *checker are resolved according to the scoping rules from the scope in
> which the checker is declared." *
> *b) Given that most vendors do not support the declaration of modules or
> checkers (same policy) within another module or checker, should we still
> allow this in the LRM? *
> *One could argue that some vendors may eventually support such a
> feature, but IMHO, this is very remote. *
> *
> *
> *_2) Read / Write of non-checker variables through hierarchical name_*
> *From my experience (even though small) with checkers, I see checkers as
> separate verification units that should not have side effects on the
> unit being verified. *
> *Thus, the writing of of non-checker variables should be avoided. *
> *The reading of non-checker variables has issues dealing with
> the scheduling regions**. Consider the following example: *
> *checker c(logic clk, a_ag); *
> * logic x, y;*
> * always (@ (posedge clk) begin*
> * ** ap_immd: assert (a_ag) else $error("a=%b", a_ag);*
> * ** // The assertion uses the a_ag as sampled in the Preponed region.*
> * ** // The $error uses the a_ag as sampled in the _Preponed _region.*
> * ** *
> * ** ap_hier: assert(test.a) else $error("a=%b", test.a);*
> * ** // The assertion uses the *test.a* as sampled in the Preponed region.*
> * ** // **The $error uses the *test.a* as sampled in the _Reactive _region.*
> * ** *
> * end *
> *endchecker : c*
> *
> *
> *module test; *
> * logic a, b, c, clk;*
> * assign a= b && c;*
> * c c1(clk, a);*
> * ... // clock statements + other stuff*
> * ** // b and c change at @ (posedge clk)*
> *
> *
> *endmodule : test*
> *Thus, I recommend that the reading of signals through hierarchical
> names should be illegal, which I think it is, but I believe taht the LRM
> is not specific about that. *
> *
> *
> *3) Allow the use of out, inout ports in checkers. *
> This brings up the same issue as above in the display of error messages.
> I think there is a mantis on this.
> Thus would also allow side effects in the DUT. The question is then, do
> we want to restrict the methodology to force checker to be strictly as
> monitors verification units, or do we want them
> to act more like modules?
> My point is that checkers should be simple verification units with no
> possible side effects.
> From my simple experience, a great percentage of checkers would most
> like be instantiated statically rather than procedurally (i.e., inside
> an always block of a module).
> Static checkers instances really behave as module instances, and if a
> user is so inclined as to create a very complex verification unit that
> communicates with the DUT and other verification units, he might as well
> use modules instead of checkers.
> Thus, unless there are very compelling reasons to allow outputs (and
> inouts) in checkers, and when we resolve this scheduling issue on the
> display of variables in action blocks, I vote against such an option.
>
> This issue needs a lot of discussions.
> Ben Cohen
>
>
>
> On Fri, Apr 23, 2010 at 1:13 AM, Kulshrestha, Manisha
> <Manisha_Kulshrestha@mentor.com <mailto:Manisha_Kulshrestha@mentor.com>>
> wrote:
>
> Hi,
>
> I think this issue if non-checker variables can be assigned inside
> checkers should be clarified. From Dimitry's email it looks like it
> is allowed but from the descriptions, it looks like it is not
> allowed. Only assignments that are discussed in the checkers chapter
> are 'checker variable assignments (17.7.1)'. Also, the LRM says that
> the functions that are used in the checkers should not have any side
> effects. So, how can someone assign a non-checker variable in the
> checker ? I think BNF allows it but not the descriptions.
>
> I think there are two parts of this issue. 1. a lower level checker
> assigning a variable from the upper level checker 2. a checker
> assigning a variable from module/program etc.
>
> Thanks.
> Manisha
>
> ------------------------------------------------------------------------
> *From:* owner-sv-ac@eda.org <mailto:owner-sv-ac@eda.org>
> [mailto:owner-sv-ac@eda.org <mailto:owner-sv-ac@eda.org>] *On Behalf
> Of *ben cohen
> *Sent:* Thursday, April 22, 2010 11:01 PM
> *To:* Korchemny, Dmitry
> *Cc:* sv-ac@server.eda.org <mailto:sv-ac@server.eda.org>
> *Subject:* Re: [sv-ac] Can checker assign value to variable outside
> its boundary?
>
> See last thread below for an example of my issue. This sentence in
> 17.2 is confusing. What does it mean?
> 17.2 "Variables used in a checker that are neither formal arguments
> to the checker nor internal variables of the
> checker are resolved according to the scoping rules from the scope
> in which the checker is declared."
>
> Also in 17.2
> "Clock and disable iff contexts are inherited from the scope of the
> checker declaration (but see 17.4 for usage of
> context value functions for passing the instantiation context to the
> checker). For example:
> module m;
> default clocking @clk1; endclocking
> default disable iff rst1;
> checker c1;
> // Inherits @clk1 and rst1
> ...
> endchecker : c1
> ...
> Am OK with that. So this in a way violates the hierarchical
> referencing requirement, but that is an exception.
> My question is then, which "Variables used in a checker that are
> neither formal arguments to the checker nor internal variables of the
> checker" is the LRM talking about?
>
> Thanks,
> Ben
>
> On Mon, Aug 24, 2009 at 12:33 AM, ben cohen <hdlcohen@gmail.com
> <mailto:hdlcohen@gmail.com>> wrote:
>
> Dmitry,
> Thanks for the explanation. Since this is an LRM, the rules
> need to be defined. I'll submitted a Mantis so as to keep track
> of this point.
>
> 0002858 <http://www.eda-stds.org/svdb/view.php?id=2858>
> Errata SV-AC major new 2009-08-24 Clarify the rules for
> assigning a value to a non-checker variable from within a checker
>
> Thanks again.
> Ben Cohen
> On Mon, Aug 24, 2009 at 12:11 AM, Korchemny, Dmitry
> <dmitry.korchemny@intel.com <mailto:dmitry.korchemny@intel.com>>
> wrote:
>
> Hi Ben,
>
>
>
> Though I don’t see any benefit in assigning a value to a
> non-checker variable in a checker, it is not formally
> forbidden in the LRM. I agree that the LRM should be
> explicit about it, and if the assignment of external
> variables is allowed, it should be stated in what region it
> is performed.
>
>
>
> The reason why all checker arguments are input is not the
> desire to disallow changing external variables in a checker,
> but it is a temporary limitation. The checkers may serve as
> building blocks for formal verification, and for this
> purpose the output checker arguments would be very useful.
> For example,
>
>
>
> checker check1(bit a, event clk); // Contains assertions
>
> bit b;
>
> check2 c(a, b, clk);
>
> assert property (@clk a |=> b);
>
> endchecker
>
>
>
> checker check2(bit a, event clk, output bit b); //
> Performs modeling
>
> always @clk
>
> b <= a;
>
> endchecker
>
>
>
> We didn’t allow output arguments in checkers because of the
> tight time schedule.
>
>
>
> Regards,
>
> Dmitry
>
>
>
> *From:* owner-sv-ac@server.eda.org
> <mailto:owner-sv-ac@server.eda.org>
> [mailto:owner-sv-ac@server.eda.org
> <mailto:owner-sv-ac@server.eda.org>] *On Behalf Of *ben cohen
> *Sent:* Monday, August 24, 2009 9:36 AM
> *To:* sv-ac@server.eda.org <mailto:sv-ac@server.eda.org>
> *Subject:* [sv-ac] Can checker assign value to variable
> outside its boundary?
>
>
>
> 17.7.1 states "It shall be illegal to reference a checker
> variable using its hierarchical name in assignments"
>
> (Note: that means that a module cannot access a checker's
> variable) That is not my question.
>
> 17.2 states "Variables used in a checker that are neither
> formal arguments to the checker nor internal variables of the
>
> checker are resolved according to the scoping rules from the
> scope in which the checker is declared."
>
> However, *nowhere in the LRM does it state that a checker
> cannot assign a value to a variable in the checker's boundary. *
>
> *Thus, by omission, it is legal to assign a value to a
> variable outside the checker's boundary. *
>
> Maybe it's a misconception on my part, *but all ports of a
> checker are inputs. The obvious intent in making ports
> inputs is prevent the assignment to objects outside the
> checker boundary. *In a way, allowing such assignments
> defeats the requirement that ports must be inputs.
>
> *_Question_*: *Can a checker assign a value to a variable in
> it's scope declaration? *
>
> Below is an example of my understanding. However, LRM is
> unclear on this.
>
> *module *test;
>
> logic *a*, b, c. clk;
>
> task t;
>
> logic t1;
>
> t1<= 1'b1;
>
> a <= t1;
>
> endtask
>
>
>
> some_other_module *m_other*; // has local variable* z*
>
>
>
> checker c(logic clk);
>
> logic x, y;
>
> always (@ (posedge clk) begin
>
> * a <= 1'b0; // ILLEGAL ?? Can write to outside
> checker boundary? *
>
> * t.t1 <= 1'b1; ILLEGAL ?? *
>
> x <= 1'b1; // OK
>
> y <= b; // OK, can read b
>
> *m_other.z <= 1'b1; // ILLEGAL* ??
>
> end
>
> endchecker : c
>
> Ben Cohen
>
>
>
>
> --
> 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* <http://www.mailscanner.info/>,
> and is
> believed to be clean.
>
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.