Turns out the LRM does indeed explain all the scenarios mentioned above.
From LRM section 16.13.6 Sequence Methods ::
The sequence on which a method is applied shall either be clocked or infer the clock from the context where it is used.
The following examples illustrate how a clock is inferred by a sequence when a method is applied to it.
module mod_sva_checks;
.......
default clocking cb @(posedge clk_d); endclocking
sequence e4;
$rose(b) ##1 c;
endsequence
// e4 infers posedge clk_a as per clock flow rules
a1: assert property (@(posedge clk_a) a |=> e4.triggered);
sequence e5;
// e4 will infer posedge clk_e1 as per clock flow rules
// wherever e5 is instantiated (with/without a method)
@(posedge clk_e1) a ##[1:3] e4.triggered ##1 c;
endsequence
// e4, used in e5, infers posedge clk_e1 from e5
a2: assert property (@(posedge clk_a) a |=> e5.matched);
sequence e6(f);
@(posedge clk_e2) f;
endsequence
// e4 infers posedge clk_e2 as per clock flow rules
a3: assert property (@(posedge clk_a) a |=> e6(e4.triggered));
sequence e7;
e4 ##1 e6(d);
endsequence
// Leading clock of e7 is posedge clk_a as per clock flow rules
a4: assert property (@(posedge clk_a) a |=> e7.triggered);
// Illegal use in a disable condition, e4 is not explicitly clocked
a5_illegal: assert property (
@(posedge clk_a) disable iff (e4.triggered) a |=> b);
always @(posedge clk_a) begin
// e4 infers default clocking cb and not posedge clk_a as there is
// more than one event control in this procedure (16.14.6)
@(e4);
d = a;
end
Similar to ‘a1’ , within ‘prop’ the sequence s1 would infer posedge clk3 as per clock flow rules.
@user49 One final question regarding ‘a5_illegal’
Why is it the ‘e4’ doesn’t infer the default clocking event ?
Is it due to ‘disable iff’ being asynchronous ?