Re: [sv-ac] 17.3.1 Behavior of instantiated checkers // Need clarifications.

Erik, Thanks for your explanation.

In a way, having a procedure within a checker behave like a standalone
procedure is an advantage because it allows the flexibility to define
assertions that are independent on where the checker is instantiated.  It
also allows the static concurrent assertions to be dependent on where the
checker is instantiated.

Thus, even though these definitions defy the natural programming intuition
that an instantiated something in procedural code should be sensitive to its
path, I see a lot of value in the decision to have a checker’s procedural
concurrent assertions behave as standalone procedural concurrent
assertions.

BTW, the next time we revisit the LRM, this point should be made more
explicitly, as it is somewhat ambiguous.  The example was clear on sum, but
not on p0.
LRM: "*Each of the three instantiations has its own version of **sum**,
which is **updated at every positive clock*
*edge, regardless of whether that instance was visited in procedural code**"
*.

I submitted a mantis for clarification.
 Summary0002891: 17.3.1 Clarification on procedural concurrent assertions
upon instantiation of checker DescriptionChange
From: "Procedural concurrent assertion statements in a checker shall be
treated just like other procedural assertion statements as described in
16.15.6"

TO: "Procedural concurrent assertion statements in a checker shall be
treated just like other procedural assertion statements as described in
16.15.6. Thus, a procedural concurrent assertion in a checker behaves as a
standalone procedural concurrent assertion, and does not inherit aspects of
its enclosing checker’s instantiation.

Thanks,
Ben Cohen



On Thu, Sep 24, 2009 at 7:55 AM, Seligman, Erik <erik.seligman@intel.com>wrote:

>  Ben—you are correct, that the two examples you give would behave
> differently.
>
>
>
> During the discussions on checkers, many committee members pointed out that
> allowing procedures within procedures would be a new, very complex semantic
> construct, and there was doubt that we could get it right.
>
>
>
> So, the decision was that we need to treat a procedure within a checker
> like a standalone procedure, rather than trying to define a way for it to
> inherit aspects of an enclosing procedure.
>
>
>  ------------------------------
>
> *From:* owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] *On
> Behalf Of *ben cohen
> *Sent:* Thursday, September 24, 2009 12:33 AM
> *To:* Abhishek Muchandikar
> *Cc:* sv-ac@eda.org; Korchemny, Dmitry; Lisa Piper; Eduard Cerny
> *Subject:* Re: [sv-ac] 17.3.1 Behavior of instantiated checkers // Need
> clarifications.
>
>
>
> Ed, Dmitry,
>
> So far I got one opinion.  I have a different opinion.  But what is the
> final read on the LRM?
>
> What is the distinction on how procedural concurrent assertion  in a
> checker are treated vs static concurrent assertions?  If treated
> differently, then what is the rationale for not having procedural concurrent
> assertion within a checker treated as if they appear at the checkers
> instantiation point.  That would mean that the following two assertions
> would behave differently in a checker:
>
>  1)    assert property(@clk a |-> b);
>
>   2) always @ (clk) begin a |-> b; end
>
> ??? puzzled!
>
> Ben
>
>
>
>
>
> On Wed, Sep 23, 2009 at 8:43 AM, ben cohen <hdlcohen@gmail.com> wrote:
>
> But the LRM makes a clear distinction on how procedural concurrent
> assertion  in a checker are treated vs static concurrent assertions.  LRM
> *does not state *that procedural concurrent assertion within a checker are
> treated as if they appear at the checkers instantiation point". Thus, I read
> this to mean that a procedural concurrent assertion in a checker is treated
> just like any other procedural concurrent assertion  instantiated in a
> module, and thus *is NOT sensitive to if(en).  * I would like some
> clarification.
>
> LRM:   *"Procedural concurrent assertion statements in a checker shall be
> treated just like other procedural*
>
> *assertion statements as descscaribed in 16.15.6. However, static
> concurrent assertion statements within a*
>
> *checker are treated as if they appear at the checker’s instantiation
> point"*
>
>
>
> On Wed, Sep 23, 2009 at 3:15 AM, Abhishek Muchandikar <
> Abhishek.Muchandikar@synopsys.com> wrote:
>
> Hi,
>
>
>
> In my opinion it is sensitive to *if (en)*
>
>
>
> Thanks
>
> Abhishek
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Wednesday, September 23, 2009 3:10 PM
> *To:* sv-ac@eda.org; Korchemny, Dmitry; Lisa Piper; Eduard Cerny
> *Subject:* [sv-ac] 17.3.1 Behavior of instantiated checkers // Need
> clarifications.
>
>
>
> Below are LRM statements,  I have 2 questions on the procedural concurrent
> assertion  instantiated in the checker as a procedural checker instance.
>
> In this LRM example, there are three instantiations of c1: check_outside,
> check_inside, and check_loop.
>
> *Question 1: *How many times will p0 be visited in any time step?
>
> once for *check_outside, *once for *check_inside *regardelss of the *en *signal,
> and 3 times in *check_loop*
>
> *Question 2*: Is p0 sensitive to the module check (*if (en*)), or is that
> ignored? Based on the text of the LRM, I would think that
>
> p0 is executed at every @ (posedge clk) and is insensitive to the
> "procedural code" surrounding the checker.
>
> Thus p0 is  added the queue regardless of the module test of *en. *
>
>
>
> Thanks,
>
> Ben
>
> // LRM stuff
>
> Procedural concurrent assertion statements in a checker shall be treated
> just like other procedural
>
> assertion statements as described in 16.15.6. However, static concurrent
> assertion statements within a
>
> checker are treated as if they appear at the checker’s instantiation point
>
>
>
> *If the checker is procedural, all static assertion statements in the
> checker are added to the pending*
>
> *procedural assertion queue for their process when the checker
> instantiation is reached in process*
>
> *execution, and then may mature or be flushed like any procedural
> concurrent assertion (see*
>
> *16.15.6.2)*
>
>
>
> Each of the three instantiations has its own version of sum, which is
> updated at every positive clock
>
> edge, regardless of whether that instance was visited in procedural code.
> Even in the case of
>
> check_loop, there is only one instance of sum, and it will be updated using
> the sampled value of
>
> in1
>
>
>
> Each of the three instantiations will queue an evaluation of p0 at every
> posedge of the clock (according
>
> to the rules in 16.15.6), which will mature and report a violation during
> any time step when sum
>
> is not less than MAX_SUM, *regardless of the behavior of the procedural
> code in module m*.
>
>
>
> checker c1(event clk, logic[7:0] a, b);
>
>   logic [7:0] sum;
>
>   always @(clk) begin
>
>      sum <= a + 1’b1;
>
>      p0: assert property (sum < `MAX_SUM);
>
>   end
>
> ..
>
> endchecker
>
>
>
> module m(...);
>
> *c1 check_outside(posedge clk, in1, in2);*
>
> always @(posedge clk) begin
>
>   automatic logic [7:0] v1=0;
>
>    *if (en*) begin  *c1 check_inside(posedge clk, in1, v1);  * end
>
>   for (int i = 0; i < 4; i++) begin
>
>    v1 = v1+5;
>
>    *if (i != 2)* begin
>
>    *c1 check_loop(posedge clk, in1, in_array[v1]);*
>
> end
>
> end
>
>
> --
> 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* <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.