RE: [sv-ac] checker: why is range not bounded by constant expression, like in modules?

From: Kulshrestha, Manisha <Manisha_Kulshrestha@mentor.com>
Date: Tue May 22 2012 - 21:35:09 PDT

Sure, it will be helpful to clarify this.

Thanks.
Manisha

From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Wednesday, May 23, 2012 9:58 AM
To: Kulshrestha, Manisha
Cc: sv-ac@eda-stds.org; Korchemny, Dmitry; Seligman, Erik; Eduard Cerny
Subject: Re: [sv-ac] checker: why is range not bounded by constant expression, like in modules?

Manisha,
Thanks, that explains it. It might be a good idea to add such an explanation in the next version.
If you feel it is worth it, I could write a mantis.
Ben

On Tue, May 22, 2012 at 9:19 PM, Kulshrestha, Manisha <Manisha_Kulshrestha@mentor.com<mailto:Manisha_Kulshrestha@mentor.com>> wrote:
Hello Ben,

As far as I understand, if the arguments passed to the checker are used as range, they must be constants. This is same as using formals in properties/sequences. It is not explicitly stated anywhere but the assertion expression after applying rewriting algorithm has to be valid.

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: Tuesday, May 22, 2012 11:41 PM

To: sv-ac@eda-stds.org<mailto:sv-ac@eda-stds.org>; Korchemny, Dmitry; Seligman, Erik; Eduard Cerny
Subject: [sv-ac] checker: why is range not bounded by constant expression, like in modules?

ISSUE: In a checker, a formal argument can define a range, which can be used in an assertion.
The actual for that range can be 1) a constant (e.g., 2, 3, or $); 2) a variable (TRUE??)
See the example below and module top.
[Ben] Where does it state that the actual argument that corresponds to a range has to be a constant? seems like it should be. The way I read the LRM, the actual could be a variable, as shown in my example in module "top".

LRM 17.3 Checker instantiation
As in the case of sequences and properties, if $ is an actual input argument to a checker instance,
then the corresponding formal argument shall be untyped and each of its references either shall be an
upper bound in a cycle_delay_const_range_expression or shall itself be an actual argument in an
instance of a named sequence or property, or in a checker instance"

checker chkr_c_test (
        input logic clk, a, b, d,
        input int min,
        input int max); // must be untyped if actual is a continuous assignment
    ap_ok_in_a_checker: assert property(@ (posedge clk)
       a |-> ##[min:max] b); // illegal in a module, legal in a checker
endchecker: chkr_c_test

module m_c_test #(mn=0, mx=20) (
        input logic clk, a, b, d,
        input int min,
        input int max); // must be untyped if actual is a continuous assignment
    ap_error_in_a_module: assert property(@ (posedge clk)
       a |-> ##[min:max] b); // illegal in a module, legal in a checker
       // Range must be bounded by constant expressions.

    ap_ok_in_module: assert property(@ (posedge clk) // using parameters
        a |-> ##[mn:mx] b);
endmodule: m_c_test

module top;
    bit clk, a=1, b=1, d;
    int min=2, max=10;
    initial forever #10 clk=!clk;
    default clocking cb_clk @ (posedge clk); endclocking

    chkr_c_test c1(clk, a, b, d, min, max); // Instance of a checker
   // SEEMS LIKE min and max sould be constants and not variables

    initial begin
      ##1 min=1; max=20;
      ##5 min=4; max=9;
    end

endmodule : top

--
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 Tue May 22 21:35:50 2012

This archive was generated by hypermail 2.1.8 : Tue May 22 2012 - 21:35:55 PDT