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, and is believed to be clean.Received on Thu Sep 24 00:38:03 2009
This archive was generated by hypermail 2.1.8 : Thu Sep 24 2009 - 00:39:30 PDT