Question

A concurrent assertion statement can also be embedded in a procedural block. For example:

property rule;
    a ##1 b ##1 c;
endproperty

always @(posedge clk) begin
    <statements>
    assert property (rule);
end

If the statement appears in an always block, the property is always monitored. If the statement appears in an initial block, then the monitoring is performed only on the first clock tick.

Two inferences are made from the procedural context: clock from the event control of an always block, and the enabling conditions.

A clock is inferred if the statement is placed in an always or initial block with an event control abiding by the following rules:

• The clock to be inferred must be placed as the first term of the event control as an edge specifier (posedge expression or negedge expression).
• The variables in expression must not be used anywhere in the always or initial block.

For example:

property r1;
    q != d;
endproperty

always @(posedge mclk) begin
    q <= d1;
    r1_p: assert property (r1);
end

The above property can be checked by writing statement r1_p outside the always block, and declaring the property with the clock as:

property r1;
    @(posedge mclk)q != d;
endproperty

always @(posedge mclk) begin
    q <= d1;
end

r1p: assert property (r1);

If the clock is explicitly specified with a property, then it must be identical to the inferred clock, as shown below:

property r2;
    @(posedge mclk)(q != d);
endproperty

always @(posedge mclk) begin
    q <= d1;
    r2_p: assert property (r2);
end

In the above example, (posedge mclk) is the clock for property r2.

Another inference made from the context is the enabling condition for a property. Such derivation takes place when a property is placed in an if...else block or a case block. The enabling condition assumed from the context is used as the antecedent of the property.

property r3;
    @(posedge mclk)(q != d);
endproperty

always @(posedge mclk) begin
    if (a) begin
        q <= d1;
        r3_p: assert property (r3);
    end
end

The above example is equivalent to:

property r3;
    @(posedge mclk)a |-> (q != d);
endproperty

r3_p: assert property (r3);

always @(posedge mclk) begin
    if (a) begin
        q <= d1;
    end
end

Similarly, the enabling condition is also inferred from case statements.

property r4;
    @(posedge mclk)(q != d);
endproperty

always @(posedge mclk) begin
    case (a)
        1: begin q <= d1;
                r4p: assert property (r4);
           end

        default: q1 <= d1;
    endcase
end

The above example is equivalent to:

property r4;
    @(posedge mclk)(a==1) |-> (q != d);
endproperty

r4_p: assert property (r4);

always @(posedge mclk) begin
    case (a)
        1: begin q <= d1;
           end
        default: q1 <= d1;
    endcase
end

The enabling condition is inferred from procedural code inside an always or initial block, with the following restrictions:

1. There must not be a preceding statement with a timing control.
2. A preceding statement shall not invoke a task call which contains a timing control on any statement.
3. The concurrent assertion statement shall not be placed in a looping statement, immediately, or in any nested scope of the looping statement.