Question

A concurrent assertion statement can be used outside of a procedural context. It can be used within a module, an interface, or a program. A concurrent assertion statement is an assert, an assume, or a cover statement.Such a concurrent assertion statement uses the always semantics.

The following two forms are equivalent:

assert property ( property_spec ) action_block
always assert property ( property_spec ) action_block ;

Similarly, the following two forms are equivalent:

cover property ( property_spec ) statement_or_null
always cover property ( property_spec ) statement_or_null

For example:

module top(input bit clk);
    logic a,b,c;

    property rule3;
        @(posedge clk) a |-> b ##1 c;
    endproperty

    a1: assert property (rule3);

    ...
endmodule

rule3 is a property declared in module top. The assert statement a1 starts checking the property from the beginning to the end of simulation. The property is always checked. Similarly,

module top(input bit clk);
    logic a,b,c;

    sequence seq3;
        @(posedge clk) b ##1 c;
    endsequence

    c1: cover property (seq3);

    ...
endmodule

The cover statement c1 starts coverage of the sequence seq3 from beginning to the end of simulation. The sequence is always monitored for coverage.