[sv-ac] question on inferred clocks

I need a clarification on the inferred clock determination for
concurrent
assertions in the procedural block. From LRM section 16.14.5, pg366,
there
are two rules to infer clock for the concurrent assertions in the
procedural
block:

1. the clock to be inferred must be placed as the first term of the
event
control as an edge specifier
  -- does this mean that the inferred clock has to be edge expression
and only
the first term? if so, what is the reason for this restriction?

for example:
     always @(posedge clk1 or negedge clk2) begin
           A1: assert property (a |=> b);
     end

  the inferred clock for A1 will be just "posedge clk1" or "posedge clk1
or negedge clk2"?

2. The variables in clock expression must not be used anywhere in the
always or
initial block.
   -- Does this mean the clock variables should not be written to or
even read in the always or initial block?


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