Section 17.10

LRM-354

Changes (in Syntax 17-15):

property_spec ::=

[clocking_event ] [ disable iff ] ( expression ) [ not ] property_expr

| [ disable iff ( expression ) ] [ not ] multi_clock_property_expr

property_expr ::=

sequence_expr

| sequence_expr |-> [ not ] sequence_expr

| sequence_expr |=> [ not ] sequence_expr

| (property_expr)

multi_clock_property_expr ::=

multi_clock_sequence

| multi_clock_sequence |=> [ not ] multi_clock_sequence

| (multi_clock_property_expr)

Section 17.11

LRM-355

Changes (in Syntax 17-16):

multi_clock_property_expr ::=

multi_clock_sequence

| multi_clock_sequence |=> [ not ] multi_clock_sequence

| (multi_clock_property_expr)

Section 17.13

LRM-349

Changes:

These example sequences are used in the following table Table 17-2 to explain the clock resolution rules for a sequence definition. The clock of any sequence when explicitly specified is indicated by X. The absence of a clock is indicated by a dash.

LRM-350

Changes:

Table 17-2: Rules for sequence definition Resolution of clock for a sequence definition

LRM-351

Changes:

Once the clock for a sequence definition is determined, the clock of a property definition is resolved similar to the resolution for a sequence definition. A single clocked property assumes that only one explicit event control can be specified. Also, the named sequences used in the property definition can contain event control in their definitions. The following table Table 17-3 specifies the rules for property definition clock resolution. The property has the form:

property p;

@(posedge p_clk) not s1 |=> s2;

endproperty

p_clk is the property for the clock, clk1 is the clock for sequence s1 and clk2 is the clock for sequence s2. The same rules apply for operator |->.

Resolution of clock for an assert statement is based on the following assumptions:

Table 17-3: Resolution of clock for an assert statement a property definition

LRM-352

Changes:

The following table Table 17-4 specifies the rules for clock resolution when assert appears in an always or initial block, where i_clk is the inferred clock from an always or initial block, d_clk is the default clock, and p_clk is the property clock.

LRM-353

Changes:

When the assert statement is outside any procedural block, there is no inferred clock. The rules for clock resolution are specified in the table below Table 17-5.