DRAFT, 12-SEP-2003 SVA 3.1A PROPOSAL: RECURSIVE PROPERTY DEFINITIONS -------------------------------------------------- DISCUSSION: ----------- 1. General This proposal extends the SVA language by allowing property definitions to be recursive. More generally, several property definitions may be mutually recursive. This proposal assumes all the provisions of the proposal on nesting implications and boolean property connectives. That proposal enables the use of property instances within property definitions, thereby opening the possibility of cyclic dependencies, hence recursive definitions. This proposal affirms the legality of recursive definitions with some restrictions. The kind of recursion created by cyclic dependencies in the property definitions corresponds to cycles in the transition graphs of automata built to check the properties. The recursion does not return and involves no stack. The recursion is required to be temporal in the sense that recursive instances are reached only after a positive temporal delay. The primary motivation for allowing recursive properties is to provide a flexible framework for coding ongoing checkerss or coverage monitors that can deal with complicated assertion requirements, such as those associated with varying numbers of data beats, out-of-order completions, retries, etc. EXAMPLE 1: Suppose we need to check write data according to the following conditions: - Each write operation can have between 1 and 16 data beats, and each data beat is 8 bits. - We have a model of the expected write data that is available at acknowledgment of a write request. - When a write request is acknowledged, it gets a 4-bit tag that is used to distinguish data beats for multiple write transactions in flight at the same time. - Data transfer for a write occurs between address acknowledgment and the last data valid, both of which have associated tags to identify the relevant write transaction. - The data beats for a single write operation occur in order. - At any time after address acknowledgment, but not later than the cycle after the last data valid, a write transaction can get the retry signal, which has an associated tag to identify the write transaction. If this happens, then the current data transfer for that write transaction is aborted and the entire data transfer will be repeated. The tag does not change and there is not a new address acknowledgment. - There is no limit on the number of times a write transaction can get the retry signal. While these conditions present a fairly complicated set of temporal requirements, they are still modest among industrial examples. They can be coded in a straightforward way, as shown below, using recursive property definitions. always @(posedge clk) assert check_write(); property check_write(); [0:127] expected_data; // local variable to sample model data [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_address_phase(expected_data, tag); endproperty property check_write_address_phase ( expected_data, // [0:127] tag // [3:0] ); first_match ( ##[0:$] (address_ack && (address_ack_tag == 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:(i*8)+7]) ) and ( (retry && (retry_tag == tag)) |=> check_write_data_beat(tag, expected_data, 4'h0) ) and ( !(retry && (retry_tag == tag)) |-> ( ( !last_data_valid |=> check_write_data_beat(tag, expected_data, i+4'h1) ) and ( (last_data_valid ##1 (retry && retry_tag == tag)) |=> check_write_data_beat(tag, expected_data, 4'h0) ) ) ) ); endproperty Notice that since there is no limit on the number of times a write transaction can get the retry signal, the recursion can go on indefinitely. This is analogous to the indefinite repetition when using an LTL "until" operator or the "[*0:$]" unbounded repetition operator. //// Recursive property definitions also allow expression of some of the weak LTL operators without introducing those operators as constructs of SVA. Here are two examples. EXAMPLE 2 (Always): If p() is a defined property, then "G p()" can be achieved by property always_p(); p() and (1'b1 |=> always_p()); endproperty Note that SVA already allows attachment of "always" at the assertion level. This recursive definition gives the semantics of "G p()" in a property that can be instantiated anywhere a property can be written [except within the scope of a negation, as excluded by Restriction 1 below]. //// EXAMPLE 3 (Weak Until): If p() and q() are defined properties, then "p() W q()" can be achieved by property p_weak_until_q(); (q()) or ( p() and (1'b1 |=> p_weak_until_q()) ); endproperty //// 2. Restrictions on Recursive Definitions The restrictions given here eliminate recursive definitions with certain pathological semantics and avoid the introduction of general liveness properties into SVA. Defined property p is said to "depend" on defined property q if there exist n >= 0 and defined properties p_0,...,p_n such that p_0 = p, p_n = q, and for all 0 <= i < n, the definition of property p_i instantiates property p_{i+1}. In particular, by taking q = p and n = 0, it follows that property p depends on property p. A defined property p has an associated "dependency digraph". The nodes of the digraph are all the defined properties on which p depends. If q and r are nodes of the digraph, then there is an arc from q to r for each instance of r in the definition of q. Such an arc is labelled by the minimum number of timesteps that are guaranteed from the beginning of the definition of q until the particular instance r. For example, if q is defined by property q(); (a |-> r()) and ((b ##1 c[*0:3]) |=> r()); endproperty where a,b,c are boolean expressions, then there is one arc from q to r labelled by "0" due to "a |-> r()" and there is a second arc from q to r labelled by "2" due to "(b ##1 c[*0:3]) |=> r()". A defined property p is called "recursive" if its node appears on a cycle in the dependency digraph of p. RESTRICTION 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. RESTRICTION 2: If p is a recursive property, then the abort operator "disable iff" cannot be applied to any instance of p that appears in the definition of any property on which p depends. This ensures that the abort condition in force cannot change during recursion. RESTRICTION 3: The sum of the arc labels around any cycle of the dependency digraph of a recursive property must be positive. In other words, any recursion must occur after a temporal advance. 3. Implementation Notes Implementation of recursive properties for simulation checking poses no conceptual difficulty, since, in principle, checkers for the various recursive threads can be coded using a programming language that supports recursion and multi-threading. For formal verification, however, a recursive property instance must be compiled into a finite representation suitable for the formal engines that will be used. The static analysis necessary to compile for formal verification can also significantly improve the performance of simulation checkers for the recursive property. The key step in compiling a recursive property instance into a suitable finite representation is to determine a finite, and hopefully small, set of instances of recursive properties on which the given property instance depends. In order to achieve this step, it must be understood that the bitwidth of each of the formal arguments to the properties is finite. Ideally, these bitwidths would be defined in the property formal arguments, but property formal arguments in SVA have no types. Therefore, the compiler must determine the maximum bitwidth needed for each formal argument of a recursive property by analyzing its definition and instances. Once the bitwidths of the formal arguments are bounded, there are only finitely many inequivalent actual argument lists for each recursive property, hence only finitely many inequivalent instances of the recursive property that are relevant for compilation. For example, if property p is defined by property p(n); ((n[0] | n[2]) |-> a) and (1'b1 |=> p(n + 1'b1)); endproperty then the instance p(x[5:0]) actually gives rise to no more than the eight instances p(x[2:0] + 3'h0), p(x[2:0] + 3'h1), ... , p(x[2:0] + 3'h7) Once a finite number of instances is obtained, then it should be possible to generate an appropriate finite representation by linking partial representations of these instances. Each such partial representation consists of a representation of the non-recursive part of the property instance, just as though the property were non-recursive, and links or transitions to the partial representation of a (possibly) different instance to account for the recursion. In the Extended CBV Statement Semantics proposed to the Accellera FVTC (3-APR-2002), it was explained in considerable detail how to build alternating automaton representations of recursive properties in this way. See http://www.eda.org/vfv/hm/att-0772/01-ecbv_statement_semantics.ps.gz In practice, of course, the number of inequivalent instances on which a recursive property instance depends may be prohibitively large. It may also be that detection of precise inequivalence is difficult, so that even if the minimum number of inequivalent instances is tractable, the computation of such a set from the assertion source is not. The LRM will not define precisely what recursive properties must compile, leaving this as an area in which the implementors can distinguish themselves. PROPOSED CHANGES TO THE BNF: ---------------------------- NONE. PROPOSED CHANGES TO LRM TEXT: ----------------------------- [TBD. There should be a section on recursive properties that captures the discussion apart from the implementation notes.] PROPOSED CHANGES TO THE FORMAL SEMANTICS: ----------------------------------------- Add the following section: G.5 Recursive Properties Defined property p is said to "depend" on defined property q if there exist n >= 0 and defined properties p_0,...,p_n such that p_0 = p, p_n = q, and for all 0 <= i < n, the definition of property p_i instantiates property p_{i+1}. In particular, by taking q = p and n = 0, it follows that property p depends on property p. A defined property p has an associated "dependency digraph". The nodes of the digraph are all the defined properties on which p depends. If q and r are nodes of the digraph, then there is an arc from q to r for each instance of r in the definition of q. Such an arc is labelled by the minimum number of timesteps that are guaranteed from the beginning of the definition of q until the particular instance r. For example, if q is defined by property q(); (a |-> r()) and ((b ##1 c[*0:3]) |=> r()); endproperty where a,b,c are boolean expressions, then there is one arc from q to r labelled by "0" due to "a |-> r()" and there is a second arc from q to r labelled by "2" due to "(b ##1 c[*0:3]) |=> r()". A defined property p is called "recursive" if its node appears on a cycle in the dependency digraph of p. RESTRICTION 1: The negation operator "not" cannot be applied to any property expression that instantiates a recursive property. RESTRICTION 2: If p is a recursive property, then the abort operator "disable iff" cannot be applied to any instance of p that appears in the definition of any property on which p depends. RESTRICTION 3: The sum of the arc labels around any cycle of the dependency digraph of a recursive property must be positive. Let p(X) be an instance of a recursive defined property p, where X denotes the actual arguments of the instance. For k >= 0, the k-fold approximation to p(X), denote p[k](X), is an instance of a non-recursive property p[k] defined inductively as follows. * The definition of p[0] is obtained from the definition of p by replacing the body property_expr with the literal "1'b1". * For k > 1, the definition of p[k-1] is obtained from the definition of p by replacing each instance of a recursive property by its (k-1)-fold approximation. The semantics of the instance p(X) is then defined as follows. For any word w over \Sigma, w |= p(X) iff for all k >= 0, w |= p[k](X).