Hi Gord, You pointed out many important and sophisticated issues, and I tried to address some of them below. I think that this item requires a general, even philosophical discussion. This proposal reflects real practical needs, and its implementation for those needs is straightforward. The complications come from corner cases and most likely would have the minimal impact in practice. Of course, this approach cannot be adopted in the LRM directly. So, what can the LRM approach be? Here are the alternatives I see: 1. LRM can entirely ignore this problem and keep the statement " The concurrent assertion statement shall not be placed in a looping statement, immediately, or in any nested scope of the looping statement." (see 16.14.5, page 368). I think that many vendors will still implement this feature, but it won't be standardized, and the assertion names will be different in different tools, and there will be no PLI access to assertions in loops. 2. We can choose a well-defined subset of limitations imposed on the loops and assertions in order to define the assertion semantics using rewriting, this is the approach of 1995. The big advantage of this approach is that there are rules describing the naming of the resulting assertions, and these rules guarantee that all the implementations synthesize the assertions with identical names. Its disadvantages you have already listed. 3. There are also compromise solutions which do not define the naming rules, but allow concurrent assertions in loops. I will explain a sketch of such definition on the following example: b1: for (int i = 1; i < 5; i++) b2: for (int j = 0; j < i; j++) // p is some property dependent on i and j a: assert property(@clk p(i,j)) pass_action(... i, j, ...); else fail_action(... i, j, ...); For the assertion semantics we will consider the loop variables as constant free variables (defined in the checker proposal). const freevar int i, j; The assertion now has the following meaning: a: assert property(@clk 0 <= i && i < 5 && 0 <= j && j < i p(i,j)) pass_action(... i, j, ...); else fail_action(... i, j, ...); i.e., the assertion a is checked for all pairs i and j meeting the loop condition predicate. This defines the formal semantics of the assertion. To complete the picture we should state that the action blocks are executed for all feasible combinations of i and j - pass or fail depending on a specific combination. Note that we don't have a problem with the assertion naming here, because we don't rewrite the assertion. Of course, simulation tools and most of FV Thanks, Dmitry -----Original Message----- From: Gordon Vreugdenhil [mailto:gordonv@model.com] Sent: Tuesday, October 30, 2007 4:16 PM To: sv-ac@eda-stds.org Subject: Mantis 1995 - concurrent assertions in loops I have taken a look over 1995 and have some of the same "structural rewrite" concerns that I've raised before. Here are some specific comments: (1) "A preceding statement shall not invoke a task call that contains a timing control on any statement." This would now require a full analysis through hierarchical task call chains of whether a task *actually has* such a delay. Either that or a sim time check that will impact performance. Why can't just void functions be used and avoid this entirely new kind of analysis? [Korchemny, Dmitry] This limitation does not introduce anything new for assertions in loops, it already exists in LRM for enable condition inference: "The enabling condition is inferred from procedural code inside an always or initial procedure, with the following restrictions: a) There must not be a preceding statement with a timing control. b) A preceding statement shall not invoke a task call that contains a timing control on any statement. ..." See 16.14.5, page 368. I am not discussing the problem itself here, and probably we should lift this limitation in all cases, but it is a separate issue, not related to this specific proposal. (2) The loop restrictions use the term "constant". That implies "constant expression" and full elaboration knowledge. If you want to have separate compilation, any restructuring of the design in the manner indicated is going to be an issue. [Korchemny, Dmitry] There are other kinds of constants required in assertions. E.g., in the assertion assert property(@clk a ##n b); n shall be a constant. Why does mentioning constants in this case introduce a new issue? (3) A foreach may have very general bounds based on the fully elaborated design. It can also refer hierarchically to the array (see Mantis 888). So the bounds are not "constant" in the assumed manner. What about a foreach over a dynamic array? An associative array? With a class handle index type? .... [Korchemny, Dmitry] I would prefer to postpone the discussion about foreach loops until the plain for loops with integer indices are understood. (4) The naming scheme says: ... loop iteration indices in square brackets shall be appended to each element of the hierarchical name that specifies a loop This is similar to the old 2001 language for hierarchical names which is entirely bogus and required a major rewrite for 2005. Such a specification could allow mixes of names from different loops since the indices are described as part of the *name*. A generate is similar to an arrayed instance with a *base name* and index *expressions*. Not describing it as such admits all sorts of questions about use of constant expressions in indices, etc. [Korchemny, Dmitry] I agree. (5) Is it now the case that one could now hierarchically reference through a *sequential* block and find a generate block? What is the relationship in terms of authoritative hierarchical names between the sequential block structure and the inferred generate? How does the pli reach these new generate blocks? Are they really in the same scope? If so, how does the pli safely deal with the different lifetime/scheduling assumptions? [Korchemny, Dmitry] One possibility is to allow PLI seeing only one original assertion. (6) Are concurrent assertions supposed to be legal in automatic contexts? If so, what do they capture and how does one know that such capture is valid? Note that one can have automatics declared inside *any* sequential block including an initial or always. [Korchemny, Dmitry] I would make illegal referencing automatic variables in concurrent assertions, at least in loops. (7) There is no statement about the enabling condition being side-effect free, non-automatic, etc. Is that stated elsewhere? What assumptions are being made about glitching behavior in the conditions? If the enable is only considered as the sampled value, won't this yield very surprising and non-intuitive results for virtually all loops with loop-variable based conditions? [Korchemny, Dmitry] It needs to be elaborated in the proposal. I don't think this proposal is nearly tight enough to be part of the LRM yet. There could be substantial impacts on assumptions and requirements for naming in other areas that have not been addressed at all. Gord. -- -------------------------------------------------------------------- Gordon Vreugdenhil 503-685-0808 Model Technology (Mentor Graphics) gordonv@model.com --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Nov 8 06:05:06 2007
This archive was generated by hypermail 2.1.8 : Thu Nov 08 2007 - 06:05:47 PST