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

Hi Erik:

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.