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

Hi Scott--
I had assumed the previous restrictions were due to the difficulty of correctly inferring the clock when complex expressions are allowed, or when expressions in the always statement also appear in the body. Since we couldn't be sure what the user intended, it's best not to infer a clock. If this is the correct rationale, then in cases where the new rule provides a clear answer, we should be OK.

If, on the other hand, the previous restriction was due to some implementation challenge of using a complex event expression to clock a procedure, or of using a procedure clock subexpression in the body, we need to revisit this.

Does anyone recall the reasoning behind the original rules disallowing a complex event expression to be used as a procedure clock, and disallowing the clock to be used in an expression?

-----Original Message-----
Ah, I see. So regarding point 1, I can infer 'posedge clk1 or negedge clk2' inside a checker by taking advantage of the forms pre-substitution, but it wouldn't be possible to do this inside a module. Am I understanding you correctly? If this sort of form is okay, then why is the rule restricting it? I don't have a good understanding of why the various restrictions are required.

Regarding point 2. I am referring to the language in the mantis. Item c states that an event must satisfy conditions 1 and 2. Condition 2 talks about the variables in the event not being used in assignments in the same procedure. My example, did not quite meet the illegal criteria. Let me try again:

Presubstitution:
always @clk1 begin
   a1: assert property(a);
   cVar1 <= var1;
   cVar2 <= var2;
end

No problems as clk1 doesn't appear in the body.

Postsubstitution:
always @(posedge clk1 or negedge clk2) begin
   a1: assert property(a);
   cVar1 <= clk1;
   cVar2 <= clk2;
end

Now the clocks appear in assignment statements in the body and in the event procedures.

This again results in a case where a checker is allowed to infer a clock where a module could not. Why this is illegal again I don't know. I think someone needs to comment on why these restrictions are needed and if it is okay for checkers to be allowed to infer these things pre-substitution even if they end up violating the rules post-substitution.

Thanks,
Scott

> -----Original Message-----
> From: Seligman, Erik [mailto:erik.seligman@intel.com]
> Sent: Friday, December 17, 2010 3:24 PM
> To: Little Scott-B11206
> Cc: Korchemny, Dmitry; sv-ac@eda.org; Francoise Martinolle
> Subject: RE: Discussion of 2804 (inferring clocking event within
> procedure)
>
> See my comments below.
>
> -----Original Message-----
> From: Little Scott-B11206 [mailto:B11206@freescale.com]
> Sent: Friday, December 17, 2010 1:13 PM
> To: Seligman, Erik
> Cc: Korchemny, Dmitry; sv-ac@eda.org; Francoise Martinolle
> Subject: 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.
>
> [Seligman, Erik] This is why we have the rule stated so you first check
> it before substitution, then *only if the first check fails* check it
> after substitution. Since the initial check on event variable clk1
> passes for the procedure in the checker, the post-substitution check is
> not done; thus we're OK that the post-substitution version doesn't fit
> the form.
>
> 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?
>
> [Seligman, Erik] Can you specify the exact line that should be
> considered illegal, and the clause in the LRM that would make it
> illegal? I'm having trouble seeing this.
>
>
> 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.