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

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, and is
believed to be clean.