[sv-ac] Fwd: P1800-2009 : 16.17 Clock resolution // quick questions

Am having a hard time understanding the following points.  Your help is
appreciated.
Ben
page 406-407
module examples_without_default (input logic a, b, c, clk);
sequence s2; $rose(a) ##[1:5] b; endsequence
sequence s3; @(negedge clk) s2; endsequence

c4: cover property (s3 ##1 b);
// illegal: no default, inferred, or explicit leading
// clocking event and maximal property is not an instance
Ben question: Why isn't s3 equivalent to:
c4: cover property (@(negedge clk) $rose(a) ##[1:5] b ##1 b);
Ben question: would this be OK?
sequence s9;   b; endsequence :
c4b: cover property (s3 ##1 s9);
---
Page 406
default clocking posedge_clk @(posedge clk); .. endclocking
property q1;  $rose(a) |-> ##[1:5] b; endproperty
property q5; @(negedge clk) b[*3] |=> !b; endproperty
property q6; q1 and q5; endproperty
a5: assert property (q6);
// illegal: default leading clocking event, @(posedge clk),
// but semantic leading clock is not unique
Page 408
The set of semantic leading clocks of q1 and q2 is the union of the set of
semantic leading clocks of q1 with the set of semantic leading clocks of q2.
Ben question: Not sure what "union of the set of semantic .." means, but in
q6, isn't that equivalent to: " @ (posedge clk) $ose(a) ->  // the default
clock
                                           ##[1:5] b    and @(negedge clk)
b[*3] |=> !b

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