[sv-ac] rules for concurent assertion clock in procedural code

Rules defined in :  16.15.6 Embedding concurrent assertions in procedural
code says:
"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."

My question is - what would be the clock for assertion as1  - would it be
inherited from always procedure clock? I have doubts as "clk" is used in
both always procedure clock and as2 assertion clock. Is this violates rule
(b) ???
 
...
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        
...
 
DANiel

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