[sv-ac] RE: Discussion of 2804 (inferring clocking event within procedure)

Hi Erik:

Let me ask a few questions to hopefully clarify my points.

1. How is 'posedge clk1 or negedge clk2' legal? I don't believe it is an event variable or a clocking block event. Assuming that is true then, "it is of the form edge_identifier expression1 [ iff expression2 ] and is not a proper subexpression of an event expression of this form." I don't see how it fits this form. To me it is of the form edge_identifier expression1 or edge_identifier expression2. Can you help me understand what I am missing? I also agree that it should be allowed, but I don't understand how the rule allows it.

2. Let's assume that 'posedge clk1 or negedge clk2' is legal. We have met condition c1 and need to also meet c2. Then doesn't my example violate condition c2? When the substitution happens the variables in expression1 are used in NBA assignments. Isn't that illegal, but would be allowed under the algorithm for applying the rules to checkers prior to the substitution and if they pass not applying the rules after the substitution?

Thanks,
Scott

> -----Original Message-----
> From: Seligman, Erik [mailto:erik.seligman@intel.com]
> Sent: Friday, December 17, 2010 2:57 PM
> To: Little Scott-B11206
> Cc: Korchemny, Dmitry; sv-ac@eda.org; Francoise Martinolle
> Subject: Discussion of 2804 (inferring clocking event within procedure)
>
>
> Hi guys-- I have been reviewing the emails on this topic, to try to
> figure out exactly what we need to discuss to properly resolve this
> item.
>
> To review, this is the currently proposed text, which we approved but
> was then rejected by the champions:
> ---------------------
> A clock shall be inferred for the context of an always or initial
> procedure that satisfies the following
> requirements:
> a) There is no blocking timing control in the procedure.
> b) There is exactly one event control in the procedure.
> c) Within the event control of the procedure, there is exactly one
> event expression that satisfies both of
> the following conditions:
> 1) The event expression consists solely of an event variable, consists
> solely of a clocking block event, or is of the form edge_identifier
> expression1 [ iff expression2 ] and is not a proper subexpression of an
> event expression of this form. If the procedure is inside a checker,
> and the event control did not satisfy this condition before the
> substitution of actual values for any event arguments to the checker,
> it shall be checked again after this substitution.
> 2) No term in expression1 expression1 appears anywhere else in the body
> of the procedure. in such a way as to affect the state of the variables
> assigned in the procedure, other than as a clocking event.
> -----------------------
>
> Here are what I believe are the key issues in John's, Scott's and
> Francoise's objections. Please clarify/respond as appropriate.
> Hopefully we can use this as a launching point for discussion in our
> next meeting.
>
>
> 1. "There is exactly one event control in the procedure". Francoise
> asks "What do you mean by one event control in the procedure? Is this
> the event control of the always/initial? or other possible event
> controls in the procedural code of the always/initial?"
> - This was actually the same text as existed pre-proposal.
> - We are assuming here that if there is only one event control, it must
> be the control associated with the always/initial at the top, not some
> mid-procedure control. But is this safe? Would it be better to say
> something explicit about the only event control being in the
> always/initial condition?
>
> 2. " If the procedure is inside a checker, and the event control did
> not satisfy this condition before the substitution of actual values for
> any event arguments to the checker, it shall be checked again after
> this substitution."
>
> 2.1. Is this a rigorous enough description of the process? Francoise
> thought it might be unclear whether we are talking about a compile-time
> or runtime check.
> - I thought this was clearly a compile-time check-- but rereading the
> description of checker arg substitution in 17.3, it's arguable that she
> is right about an ambiguity there.
>
> 2.2. For the pre-substitution check, John raised this question: is a
> checker input variable considered an event variable for the purpose of
> this check? So if we have a checker input e and a procedure is clocked
> by "@e", will the pre-subsitution check pass and thus set the procedure
> to be clocked by e?
> - I would think yes-- not sure of the claimed source of ambiguity.
> - Remember, we added this clause so we could pass some compound event
> like 'posedge clk1 or negedge clk2' to a checker & have this compound
> expression actually clock procedures.
>
> 2.3. Following the above rule, suppose we do pass in something like
> "posedge clk1 or negedge clk2" to a checker, and it thus becomes a
> procedure's clock. (This is illustrated in Scott's email below.) If
> I'm interpreting right, John and Scott are worried that this may be
> illegal.
> - It looks to me like clause 9.4.2.1 explicitly permits compound
> events. Am I missing some constraint?
>
>
> 3. The phrase ""in such a way as to affect the state of the variables
> assigned in the procedure, other than as a clocking event" may be
> problematic.
> - Can we replace with simply ",other than as a clocking event or in
> assertion statements"? What usages would this impact?
>
>
>
> -----Original Message-----
> From: Little Scott-B11206 [mailto:B11206@freescale.com]
> Sent: Tuesday, December 14, 2010 12:49 PM
> To: Seligman, Erik
> Cc: Korchemny, Dmitry
> Subject: Example for 2804
>
> Hi Erik:
>
> Below is an example that I believe highlights John's concern. The way
> I read the rules with a nudging from John is that if we look at the
> checker pre-substitution everything looks fine and it would pass the
> check. My understanding is that no further checking would be don post-
> substitution. If we look at the notOk instantiation of the checker
> there are now issues that would prevent the clock from being inferred
> if we also checked post-substitution.
> 1. clk1 is posedge clk1 or negedge clk2 which I don't think can be used
> as an inferred clock. Is that correct? That is how I read the
> restrictions, but I don't intuitively understand why that is the case.
> 2. clk1 and clk2 are used in the clocking event and also in an
> assignment
>
> One other item in the mantis that I struggled with is that I couldn't
> find a description of how/when the substitution happens with checkers.
> Can you point me to the spot in the LRM where this is described? If it
> isn't well described do we need to use language other than
> substitution?
>
> Thanks,
> Scott
>
> checker pure_evil (
> event clk1,clk2
> untyped var1, var2, a, b
> );
>
> bit cVar1, cVar2;
>
> always @clk1 begin
> a1: assert property(a);
> end
>
> always @clk2 begin
> cVar1 <= var1;
> cVar2 <= var2;
> end
>
> endchecker : pure_evil
>
> Then it is instantiated as:
>
> pure_evil itsOk(.clk1(posedge clk1),
> .clk2(negedge clk2),
> .var1(foo),
> .var2(bar),
> .*
> );
> pure_evil notOk(.clk1(posedge clk1 or negedge clk2),
> .clk2(posedge clk2),
> .var1(clk1),
> .var2(clk2)
> .*
> );
>
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.