In reply to MICRO_91:
The key to understanding multiclocking is to understand that a clock flow into a parenthesized (or declared) sequence, but it does not flow out of it. I explain clock flow in my book. Here is a section of it.
I also made some misstatements
But I am puzzled by
ap1a:assert property ( @(posedge clk0) A |=> mclocks ) ; // *** ILLegal
// ILLEGAL by tool vendors. I thought that the clock would flow into the sequence
//BUT the following is OK
ap1b:assert property ( @(posedge clk0) A |=> (@(posedge clk1) B and @(posedge clk2) C));
Thus,
module lce;
bit clk, clk0, clk1, clk2, a, b, c, d, e;
initial forever #10 clk=!clk;
// Illegal, no leading clocking event
ap_and2_seq_ERROR: assert property(
(@ (posedge clk) a ##1 b) and
(c ##2 d) // illegal
);
// Illegal, no leading clocking event
// both sequences start concurrently
ap_and2_seq_ERROR2: assert property(
(@ (posedge clk) a ##1 b) and
(@ (posedge clk2) c ##2 d)
); // has multiple leading clocks for its maximal property
// OK, one leading clocking event
ap_and2ab: assert property(@ (posedge clk0) 1|->
(@ (posedge clk) a ##1 b) and
(@ (posedge clk2) c ##2 d)
);
// Illegal, no leading clocking event
// both properties start concurrently
ap_and2_Prop_ERROR: assert property(
(@ (posedge clk) 1 |-> a ##1 b) and
(@ (posedge clk2) 1 |-> c ##2 d)
);
// OK, Same leading clocking event
// both properties start concurrently
ap_and2_Prop_OK_same_clk: assert property(
(@ (posedge clk) 1 |-> a ##1 b) and
(@ (posedge clk) 1 |-> c ##2 d)
);
ap_and2_Prop_OK: assert property(@ (posedge clk0) 1 |->
(@ (posedge clk) 1 |-> a ##1 b) and
(@ (posedge clk2) 1 |-> c ##2 d)
);
ap_mult_clk: assert property(
@ (posedge clk1) a [*0:1] ##1 // illegal a[*0] is empty
@ (posedge clk2) b[*0:2] ##1 c); // illegal b[*0] is empty
endmodule : lce