[sv-ac] 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.