Question

下面的例子演示了特性的格式。

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

property rule2;
    @(clkev)
        disable iff (foo)
            a |-> not(b ##1 c ##1 d);
endproperty

特性rule2对蕴含中后项的(b ##1 c ##1 d)序列取反。clkev为特性指定了时钟。

property rule3;
    @(posedge clk)
        a[*2] |-> ((##[1:3] c) or (d |=> e));
endproperty

Property rule3 says that if a holds and a also held last cycle, then either c must hold at some point 1 to three cycles after the current cycle, or, if d holds in the current cycle, then e must hold one cycle later.

property rule4;
    @(posedge clk)
        a[*2] |-> ((##[1:3] c) and (d |=> e));
endproperty

Property rule4 says that if a holds and a also held last cycle, then c must hold at some point 1 to three cycles after the current cycle, and if d holds in the current cycle, then e must hold one cycle later.

property rule5;
    @(posedge clk)
        a ##1 (b || c)[->1] |->
            if (b)
                (##1 d |-> e)
            else // c
                f;
endproperty

Property rule5 has a followed by the first match of either b or c as its antecedent. The consequent uses if...else to split cases on which of b or c is matched first.

property rule6(x,y);
    ##1 x |-> y;
endproperty

property rule5a;
    @(posedge clk)
        a ##1 (b || c)[->1] |->
            if (b)
                rule6(d,e)
            else // c
                f;
endproperty

特性rule5a等价于rule5，但它使用rule6的一个实例作为一个特性表达式。

一个特性可以可选地为时钟指定一个事件控制。时钟派生和解析的规则将在17.14节中描述。

一个命名特性可以通过引用它的名字来实例化。与SystemVerilog命名约定一致，我们可以使用一个层次化的名字。像序列声明一样，对于在一个特性中使用并且不是特性的形式参数的变量，它们从特性被声明的作用域中进行层次化的解析。

使用多个时钟的特性将在17.12节中描述。