1800’2017: 16.16 Clock resolution addresses this topic.
1) Using default clocking block: LEGAL
default clocking cb1 @(posedge clk); endclocking
sequence sr1; a ##2 b ; endsequence
property pr1; c |=> sr1; endproperty
ap1:assert property(pr1); // LEGAL
**2) Specifying clock in sequence: LEGALITY DEPENDS ON USE/b]
See embedded comments
sequence sr1; @(posedge clk) a ##2 b; endsequence
property pr1; c |=> sr1; endproperty
ap2:assert property(pr1); // ILLEGAL
// Illegal because c has no leading clocking event (LCE)
// the clocking event in sr1 does not flow backwards
//-----------
property pr2; sr1 |-> c; endproperty
// Directive 'ap2' has un-clocked expressions or constructs. Please fix
ap2b:assert property(pr2); // ILLEGAL
// The clocking event in sr1 does not flow out of the sequence
//--------------
sequence s2; @(posedge clk) a ##2 b; endsequence
property p2; not s2; endproperty
assert property (p2); // LEGAL because the s2 has a LCE
[b]Specifying clock in property: DEPENDS**
sequence sr1; a ##2 b ; endsequence
property pr1; @(posedge clk) c |=> sr1; endproperty
ap3:assert property(pr1); LEGAL
// Clocking event in property is the LCE and
// it flows into sr1. It cannot flow out of the sequence
// but can flow into sequences following the sr1
property pr1b; @(posedge clk) c |=> sr1 ##1 d; endproperty
// -----
sequence sq; a ##2 b ; endsequence
property p1x; @(posedge clk) c |=> sq; endproperty
property p2x; @(posedge clk2) c |=> a ##1 sq; endproperty
ap3:assert property(pr1); // LEGAL
ap4: assert property(p1 implies p2x);// illegal
// Directive 'ap3' has un-clocked expressions or constructs
4) Clock Inferred from always block: LEGAL
sequence sr1; seq ##2 gnt ; endsequence
property pr1; cStart |=> sr1; endproperty
always@(posedge clk) ap4:assert property(pr1);
// Infers the clock from always block
5) Clock inferred from forever block is ILLEGAL
sequence sr1b; req ##2 gnt ; endsequence
property pr1b; cstart |=> sr1; endproperty
initial begin
forever @(posedge clk) begin
// The sva directive is not sensitive to a clock. .
// Procedural assertion ( i.e., assert, assume or cover property) is not
// allowed in looping statement.Only immediate assertions are allowed in this
ap5:assert property(pr1b);
The same rules do apply for cover property as well ?
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog