[sv-ac] Q: fix for rule (b) in 16.15.6 to allow inferred clock when expression appears in procedural assertion

I have the action item to put together a proposal for this one.
It's looking to me like it might be a simple change to rule (b):

b) No term in expression1 appears anywhere else in the body of the procedure, except in a concurrent assertion statement or checker instantiation.

Does anyone think this needs to be something more complicated?

>"Within the event control of the procedure, there is exactly one event
>expression that satisfies both of the following conditions:
>
>a) The event expression is of the form edge_identifier expression1 [ iff
>expression2 ] and is not a proper subexpression of an event expression
>of
>this form.
>
>b) No term in expression1 appears anywhere else in the body of the
>procedure."
>
>However, look at this example:
>------------
>default clocking dclk @(posedge clk);endclocking
>//<<<------- clk used in default clocking
>always @(negedge clk) begin //clk used in event
>control in procedural code
> as1: assert property (a ##1 a);
> as2: assert property (@(posedge clk) a ##1 a);
>//<<<-------- clk used inside body of the procedure
>
>end
>
>-----------
>
>I believe most of us would think negedge clk should be inferred as the
>clock for as1, but a literal reading of rule b would force a non-
>inference of the clocking event due to the use of clk in as2. In this
>interpretation, as1 would get the default clock.
>
>Thus, we may need an exception to rule (b) to state that appearances of
>the clocking event inside concurrent assertion statements are OK.
>

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