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

From: Korchemny, Dmitry <dmitry.korchemny@intel.com>
Date: Tue Apr 27 2010 - 08:49:15 PDT

This fragment exists in the released LRM. See at the bottom of page 432.

Regards,
Dmitry

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Monday, April 26, 2010 9:27 PM
To: Thomas Thatcher
Cc: Kulshrestha, Manisha; Korchemny, Dmitry; sv-ac@server.eda.org
Subject: Re: [sv-ac] Can checker assign value to variable outside its boundary?

17.2, page 418 of IEEE 1800-2009 D9 version has
"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."
That's the only copy I have. It might have deleted in the IEEE released version.

So I don't think that we can drop 2858 so easily
Agree There are issues to discuss.
Ben Cohen

On Mon, Apr 26, 2010 at 10:24 AM, Thomas Thatcher <thomas.thatcher@oracle.com<mailto:thomas.thatcher@oracle.com>> wrote:
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> <mailto: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>>
   [mailto: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> <mailto: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>
   <mailto: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> <mailto: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>>
           [mailto: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> <mailto: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.
---------------------------------------------------------------------
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 Tue, 27 Apr 2010 18:49:15 +0300

This archive was generated by hypermail 2.1.8 : Tue Apr 27 2010 - 08:50:21 PDT