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

From: Kulshrestha, Manisha <Manisha_Kulshrestha@mentor.com>
Date: Fri Apr 23 2010 - 01:13:21 PDT

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] On Behalf Of ben cohen
Sent: Thursday, April 22, 2010 11:01 PM
To: Korchemny, Dmitry
Cc: 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> 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> 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] On Behalf Of ben cohen
                Sent: Monday, August 24, 2009 9:36 AM
                To: 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, and is
believed to be clean.
Received on Fri Apr 23 01:17:27 2010

This archive was generated by hypermail 2.1.8 : Fri Apr 23 2010 - 01:17:44 PDT