Hi Erik, Checkers don't essentially introduce always blocks within other always blocks since the checker instantiation is not an inlining in place, this is similar to concurrent assertions. always @(posedge clk) p: assert property(a); does not mean that the assertion p is executed when the control flow reaches it, but is only syntax to infer the assertion clock, and is equivalent to p: assert property(@(posedge clk) a; If you instantiate a checker within an always block always @(posedge clk) mycheck p(a); and mycheck itself has an always block, it does not mean that we have a nested always block: the checker's always block should be thought to be an independent always block (not nested). The only purpose of checker instantiation within the always block is the context inference. E.g., if mychecker is defined as: checker mychecker(x, clock = $inferred_clock); then clock will be inferred as posedge clk, and therefore the above instantiation is equivalent to: mycheck p(a, posedge clk); I think, this answers Lisa's question: in the example below (copying it here for convenience): default disable my_disable; always @(posedge clk) begin ... // checker will inherit posedge clk, my_disable mycheck mycheck1(.a(a),.b(b)); ... end ... checker mycheck(a,b, clk2, clk = $inferred_clk, rst = $inferred_rst); default disable rst;... // p1 inherits clock and disable from calling context p1: assert property @(posedge clk) (a); always @(posedge clk2) // No inferences here, since inside new always block. p2: assert property (b); ... endchecker p2 is controlled by posedge clk2 regardless of mycheck instantiation. Instantiating mycheck within the always block affects *only* the value of clk in the checker (BTW I think that @(posedge clk) in p1 is a typo, it should be @clk1 - you cannot specify posedge of an arbitrary event). As for Erik's comment, the answer is that it is the responsibility of the checker implementer to take this situation into account. To make the behavior of always @(posedge clk or negedge rstnn) if (!rstnn) mycheck(foo,bar,clk); intuitive, the checker has to be written as: checker mycheck(a,b, clk2, clk = $inferred_clk, rst = $inferred_rst, en = $inferred_enable); default disable rst;... // p1 inherits clock and disable from calling context p1: assert property @(posedge clk) (en|->a); always @(posedge clk2) // No inferences here, since inside new always block. p2: assert property (en|->b); ... endchecker Thanks, Dmitry ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Seligman, Erik Sent: Friday, July 27, 2007 9:02 PM To: Lisa Piper Cc: sv-ac@server.eda-stds.org Subject: RE: [sv-ac] Feedback on 1900 (new 'checker' construct) Hi guys-- I think I've just about caught up with my email. One issue that sticks out as possibly requiring further discussion is the probelm of a potential 'always' within an 'always'. Lisa's example below shows a good reason we need to allow this, to meet our goal of enabling generalized OVL-like libraries: 'mycheck' can now be used both outside an always loop (like current OVL checkers), and inside an always loop. If we did not allow the always within a checker, we could not do this. I believe the semantics we currently had in mind is that the new always completely overrides the previous context. However, as I stare at this, I'm wondering if this may lead to some counter-intuitive results. For example. suppose a DE has been given a library including the 'mycheck' below (without the default_disable), and uses it in the following code: always @(posedge clk or negedge rstnn) if (!rstnn) mycheck(foo,bar,clk); A reasonable designer might think they have accounted for the reset case, since the checker is inside an 'if (!rstnn)'. But from the proposal as we have it now, it looks to me like p2 will be checked even during reset. Perhaps this is unavoidable if we want to support 'always' within checkers. A bit ugly, but with a correctly written checker library that handles all the inferred values reasonably, it should be fine. On the other hand, is there a better way to define things & make these cases simpler? ________________________________ default disable my_disable; always @(posedge clk) begin ... // checker will inherit posedge clk, my_disable mycheck mycheck1(.a(a),.b(b)); ... end ... checker mycheck(a,b, clk2, clk = $inferred_clk, rst = $inferred_rst); default disable rst;... // p1 inherits clock and disable from calling context p1: assert property @(posedge clk) (a); always @(posedge clk2) // No inferences here, since inside new always block. p2: assert property (b); ... Endchecker The other thing that makes this complex is in essence having an always block within an always block. How does this work? Is it only when both events occur? Is it legal to have different clocks? I think the example that Dimitry sent was very simple and clear. Lisa ________________________________ From: Lisa Piper Sent: Monday, July 23, 2007 3:23 PM To: 'Seligman, Erik'; sv-ac@eda-stds.org Subject: RE: [sv-ac] Feedback on 1900 (new 'checker' construct) Erik, I have reviewed the checker proposal. The application and use model for this is still not clear to me. How does this compare with using parametized properties in a package? My biggest concern is that this is yet another way that things could be done. The average user is going to become overwhelmed with trying to understand the alternatives. More specific questions: 1. You state that it is similar to a PSL vunit, A PSL vunit is essentially an extension of the module scope. It has the advantage over SVA bind that you do not have to bundle the code into a module with a complete port list. The signals in the vunit connect to the signals of the same name in the associated module. But you still need to know the names of the signals in the design, which resticts re-use. And it does not allow for instantiating a checker in procedural code as you have shown in these examples. (Note that PSL is adding parameter lists to vunits to address the reuse issue.) 2. How will checkers be documented to make the use easy? Is it only the clock and disable that can be inferred from context? How does the user know what will be inferred? It would be very confusing from a debug perspective if some properties do infer and some do not, as shown in example 3. My fear is that it will be as difficult to learn libraries as it is to just learn the underlying language. 3. To debug a failure, won't the user need to be able to understand SVA? Is the goal of the user not needing to understand SVA realistic or desired? 4. This will allow always blocks within always blocks, where the top level always block has what effect? 5. Instantiation of a 'checker' inside an 'always' block makes this equivalent to a kind of module inside an always block. This is against the Verilog language in general. It also allows user to put things inside an always block which are not otherwise legal in Verilog (e.g assign statements). This will make things confusing without any real benefit. 6. There is a statement that checkers may not include module, interface, or cell declarations or instantiations. What is a "cell"? 7. In example 4, is this PSL? Will PSL be allowed in a checker? ovl_width_a1: assert always ((checking & !test_sig) |-> (t >= width)) 8. How is a free variable different from a local variable? The bottom line is that I do not see any compelling reason for this new construct. Lisa -----Original Message----- From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik Sent: Monday, July 23, 2007 2:54 PM To: sv-ac@eda-stds.org Subject: [sv-ac] Feedback on 1900 (new 'checker' construct) Hi guys-- I'm going to start working on the 'real' proposal (manual format) for item 1900. Please try to send any feedback you have at this point. Thanks! -- This message has been scanned for viruses and dangerous content by MailScanner, 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.Received on Sat Jul 28 23:35:25 2007
This archive was generated by hypermail 2.1.8 : Sat Jul 28 2007 - 23:36:02 PDT