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

Hi Ben,

my reading of the lrm is that yes, these two assertions will behave differently, 1 is triggered by control reaching the checker instance in the procedure, 2 is not.

Best regards,
ed

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Thursday, September 24, 2009 3: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<mailto: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<mailto: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> [mailto: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<mailto: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, and is
believed to be clean.