Question

SystemVerilog具有多种方法为一个特性指定时钟。

— 具有一个时钟的序列实例，例如：

sequence s2;
    @(posedge clk)
        a ##2 b;
endsequence

property p2;
    not s2;
endproperty

assert property(p2);

— 特性，例如：

property p3; @(posedge clk) not (a ##2 b); endproperty
assert property (p3);

— contextually inferred clock from a procedural block, for example:

always @(posedge clk) assert property (not (a ##2 b));

— clocking block, for example:

clocking master_clk @(posedge clk);
    property p3; not (a ##2 b); endproperty
endclocking
assert property (master_clk.p3);

— default clock, for example:

default clocking master_clk ; // master clock as defined above
property p4; (a ##2 b); endproperty
assert property (p4);

For a multi-clocked assertion, the clocks are explicitly specified. No default clock or inferred clock is used. In addition, multi-clocked properties are not allowed to be defined within a clocking block.

A multi-clocked property assert statement must not be embedded in procedural code where a clock is inferred.For example, following forms are not allowed.

always @(clk) assert property (mult_clock_prop);// illegal
initial @(clk) assert property (mult_clock_prop);// illegal

The rules for an assertion with one clock are discussed in the following paragraphs.

The clock for an assertion statement is determined in the decreasing order of priority:

1. Explicitly specified clock for the assertion.
2. Inferred clock from the context of the code when embedded.
3. Default clock, if specified.

A concurrent assertion statement must resolve to a clock. Otherwise, the statement is considered illegal.

Sequences and properties specified in clocking blocks resolve the clock by the following rules:

1. Event control of the clocking block specifies the clock.
2. No explicit event control is allowed in any property or sequence declaration.
3. If a named sequence that is defined outside the clocking block is used , its clock, if specified, must be identical to the clocking block’s clock.
4. Multi-clock properties are not allowed.

Resolution of clock for a sequence declaration assumes that only one explicit event control can be specified. Also, the named sequences used in the sequence declaration can, but do not need to, contain event control in their definitions.

sequence s;
    //sequence composed of two named subsequences
    @(posedge s_clk) e ##1 s1 ##1 s2 ##1 f;
endsequence

sequence s1;
    @(posedge clk1) a ##1 b; // single clock sequence
endsequence

sequence s2;
    @(posedge clk2) c ##1 d; // single clock sequence
endsequence

These example sequences are used in Table 17-3 to explain the clock resolution rules for a sequence declaration. The clock of any sequence when explicitly specified is indicated by X. Otherwise, it is indicated by a dash.

Table 17-3: Resolution of clock for a sequence declaration

s_clk	clk1	clk2	Resolved clock	Semantic restriction
-	-	-	unclocked	-
X	-	-	s_clk	-
X	X	-	s_clk	s_clk and clk1 must be identical
X	X	X	s_clk	s_clk, clk1 and clk2 must be identical
X	-	X	s_clk	s_clk and clk2 must be identical
-	X	-	unclocked	-
-	X	X	unclocked	clk1 and clk2 must be identical
-	-	X	unclocked	-

Once the clock for a sequence declaration is determined, the clock of a property declaration is resolved similar to the resolution for a sequence declaration. A single clocked property assumes that only one explicit event control can be specified. Also, the named sequences used in the property declaration can contain event control in their declarations. Table 17-4 specifies the rules for property declaration 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 |->.

Table 17-4: Resolution of clock for a declaration

p_clk	clk1	clk2	Resolved clock	Semantic restriction
-	-	-	unclocked	-
X	-	-	p_clk	-
X	X	-	p_clk	p_clk and clk1 must be identical
X	X	X	p_clk	p_clk, clk1 and clk2 must be identical
X	-	X	p_clk	p_clk and clk2 must be identical
-	X	-	unlocked	-
-	X	X	unlocked or multi-clock	clk1 and clk2 must be identical. If clk1 and clk2 are different for the case of operator |=>, then it is considered a multi-clock implication
-	-	X	unlocked	-

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

• assert can appear in an always block, initial block or outside procedural context
• clock is inferred from an always or initial block
• default clock can be specified using default clocking block

Table 17-5 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.

Table 17-5: Resolution of clock in an always or initial block

i_clk	d_clk	p_clk	Resolved clock	Semantic restriction
-	-	-	unclocked	Error. An assertion must have a clock
X	-	-	i_clk	-
-	X	-	d_clk
-	-	X	p_clk
X	-	X	i_clk	i_clk and p_clk must be identical
X	X	-	i_clk	-
-	X	X	p_clk
-	-	X	p_clk	-

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

Table 17-6: Resolution of clock outside a procedural block

d_clk	p_clk	Resolved clock	Semantic restriction
-	-	unlocked	Error. An assertion must have a clock
X	-	d_clk
-	X	p_clk
X	X	p_clk