Question

SystemVerilog允许使用递归的特性。如果一个命名特性的声明调用了其本身的一个实例，那么这个命名特性是递归的。递归提供了一种灵活的框架来对特性进行编码以便作为正在进行的假设、检查器或覆盖率监视器使用。

例如：

property prop_always(p);
    p and (1'b1 |=> prop_always(p));
endproperty

上述例子是一个递归特性，它表示作为形式参数的特性p必须在每一个周期保持。如果特性p保持的正在进行的需求在一个在序列s中编码的复杂的触发条件之后施加的话，这个例子非常有用。

property p1(s,p);
    s |=> prop_always(p);
endproperty

另外一个例子：

property prop_weak_until(p,q);
    q or (p and (1'b1 |=> prop_weak_until(p,q)));
endproperty

上述的递归特性表示作为形式参数的特性p必须在每一个周期保持直到（但不包括）作为形式参数的特性q保持的第一个周期。尽管作为形式参数的特性q并不要求永远保持。This example is useful if p must hold at every cycle after a complicated triggering condition encoded in sequence s, but the requirement on p is lifted by q:

property p2(s,p,q);
    s |=> prop_weak_until(p,q);
endproperty

More generally, several properties can be mutually recursive. For example

property check_phase1;
    s1 |-> (phase1_prop and (1'b1 |=> check_phase2));
endproperty

property check_phase2;
    s2 |-> (phase2_prop and (1'b1 |=> check_phase1));
endproperty

递归的特性声明具有三个限制。

限制1：The negation operator not cannot be applied to any property expression that instantiates a recursive property. In particular, the negation of a recursive property cannot be asserted or used in defining another property.

Here are examples of illegal property declarations that violate Restriction 1:

property illegal_recursion_1(p);
    not prop_always(not p);
endproperty

property illegal_recursion_2(p);
    p and (1'b1 |=> not illegal_recursion_2(p));
endproperty

限制2：The operator disable iff cannot be used in the declaration of a recursive property. This restriction is consistent with the restriction that disable iff cannot be nested.

Here is an example of an illegal property declaration that violates Restriction 2:

property illegal_recursion_3(p);
    disable iff (b)
        p and (1'b1 |=> illegal_recursion_3(p));
endproperty

The intent of illegal_recursion_3 can be written legally as

property legal_3(p);
    disable iff (b) prop_always(p);
endproperty

since legal_3 is not a recursive property.

限制3：If p is a recursive property, then, in the declaration of p, every instance of p must occur after a positive advance in time. In the case of mutually recursive properties, all recursive instances must occur after positive advances in time.

Here is an example of an illegal property declaration that violates Restriction 3:

property illegal_recursion_4(p);
    p and (1’b1 |-> illegal_recursion_4(p));
endproperty

If this form were legal, the recursion would be stuck in time, checking p over and over again at the same cycle.

Recursive properties can represent complicated requirements, such as those associated with varying numbers of data beats, out-of-order completions, retries, etc. Here is an example of using a recursive property to check complicated conditions of this kind.

EXAMPLE: Suppose that write data must be checked according to the following conditions:

• Acknowledgment of a write request is indicated by the signal write_request together with write_request_ack. When a write request is acknowledged, it gets a 4-bit tag, indicated by signal write_reqest_ack_tag. The tag is used to distinguish data beats for multiple write transactions in flight at the same time.
• It is understood that distinct write transactions in flight at the same time must be given distinct tags. For simplicity, this condition is not a part of what is checked in this example.
• Each write transaction can have between 1 and 16 data beats, and each data beat is 8 bits. There is a model of the expected write data that is available at acknowledgment of a write request. The model is a 128-bit vector. The most significant group of 8 bits represents the expected data for the first beat, the next group of 8 bits represents the expected data for the second beat (if there is a second beat), and so forth.
• Data transfer for a write transaction occurs after acknowledgment of the write request and, barring retry, ends with the last data beat. The data beats for a single write transaction occur in order.
• A data beat is indicated by the data_valid signal together with the signal data_valid_tag to determine the relevant write transaction. The signal data is valid with data_valid and carries the data for that beat. The data for each beat must be correct according to the model of the expected write data.
• The last data beat is indicated by signal last_data_valid together with data_valid and data_valid_tag. For simplicity, this example does not represent the number of data beats and does not check that last_data_valid is signaled at the correct beat.
• At any time after acknowledgement of the write request, but not later than the cycle after the last data beat, a write transaction can be forced to retry. Retry is indicated by the signal retry together with signal retry_tag to identify the relevant write transaction. If a write transaction is forced to retry, then its current data transfer is aborted and the entire data transfer must be repeated. The transaction does not rerequest and its tag does not change.
• There is no limit on the number of times a write transaction can be forced to retry.
• A write transaction completes the cycle after the last data beat provided it is not forced to retry in that cycle.

Here is code to check these conditions:

property check_write;
    logic [0:127] expected_data; // local variable to sample model data
    logic [3:0] tag; // local variable to sample tag

    disable iff (reset)
    (
        write_request && write_request_ack,
        expected_data = model_data,
        tag = write_request_ack_tag
    )
    |=>
        check_write_data_beat(expected_data, tag, 4’h0);
endproperty

property check_write_data_beat
(
    expected_data, // [0:127]
    tag, // [3:0]
    i // [3:0]
);

    first_match
    (
        ##[0:$]
        (
            (data_valid && (data_valid_tag == tag))
            ||
            (retry && (retry_tag == tag))
        )
    )
    |->
    (
       (
           (data_valid && (data_valid_tag == tag))
           |->
           (data == expected_data[i*8+:8])
       )
       and
       (
           if (retry && (retry_tag == tag))
           (
               1’b1 |=> check_write_data_beat(tag, expected_data, 4’h0)
           )
           else if (!last_data_valid)
           (
               1’b1 |=> check_write_data_beat(tag, expected_data, i+4’h1)
           )
           else
           (
               ##1 (retry && (retry_tag == tag))
               |=>
               check_write_data_beat(tag, expected_data, 4’h0)
           )
       )
    );
endproperty