Question

A property on its own is never evaluated for checking an expression. It must be used within a verification statement for this to occur. A verification statement states the verification function to be performed on the property. The statement can be one of the following:

• assert to specify the property as a checker to ensure that the property holds for the design
• assume to specify the property as an assumption for the environment
• cover to monitor the property evaluation for coverage

A concurrent assertion statement can be specified in:

• an always block or initial block as a statement, wherever these blocks can appear
• a module
• an interface
• a program

procedural_assertion_statement ::=         // from Annex A.6.10
    concurrent_assertion_statement
  | immediate_assert_statement

concurrent_assertion_item ::=             // from Annex A.2.10
    [block_identifier :] concurrent_assertion_statement

concurrent_assertion_statement ::=
    assert_property_statement
  | assume_property_statement
  | cover_property_statement

assert_property_statement::=
    assert property (property_spec) action_block

assume_property_statement::=
    assume property (property_spec);

cover_property_statement::=
    cover property (property_spec) statement_or_null

Syntax 17-16—Concurrent assert construct syntax (excerpt from Annex A)

The assert, assume or cover statements can be referenced by their optional name. A hierarchical name can be used consistent with the SystemVerilog naming conventions. When a name is not provided, a tool shall assign a name to the statement for the purpose of reporting. Assertion control system tasks are described in Section 23.9.