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

Hi Erik,

regarding the last point I think that this relates to how clocks are recognized when synthesizing hardware. The clock itself is not explicitly used in the body of the always procedure.

ed

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Seligman, Erik
> Sent: Tuesday, December 28, 2010 5:36 PM
> To: Little Scott-B11206
> Cc: Korchemny, Dmitry; sv-ac@eda.org; Francoise Martinolle
> Subject: [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.
>

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