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

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