Subject: some additional requirements
From: Erich Marschner (erichm@cadence.com)
Date: Wed Jul 31 2002 - 20:33:13 PDT
Following are some proposed additional requirements for System Verilog assertions. This is not intended to be an exhaustive list - I have not intentionally repeated requirements that others have already mentioned, or that were listed in the FVTC requirements. Instead, they are for the most part additional requirements that, to my knowledge, have not been mentioned elsewhere.
Regards,
Erich
=======================================================================
Some Additional Requirements for System Verilog Assertions
1. Support a methodology that allows the user to NOT have to tell the verification tool what to do with each 'assertion' (or 'property').
Justification:
Designs are hierarchical, and verification is generally done by parts, at least much of the time. Whether a given property specification functions as an assertion (to be proven) or an assumption (to be assumed now and proven later) or as a special-case restriction (to be assumed temporarily, although it is not provable) depends in part on what portion of the design is being verified at the moment. (Generally we can only assume a property that is dependent upon primary inputs of the subsection of the design currently being verified.) A methodology in which the user is required to label each property as an assertion, an assumption, or a restriction could cause the designer to continually edit source code in order to change the sense of each property to match the current verification run - and this could introduce accidental errors. A better methodology is one in which the user specifies properties (or assertions) in the code, but the decision whether to check or assume a given property is made either by th
e tool, automatically, or by the too user, outside the source code. The language may still provide a means of explicitly asserting or assuming a given property, but if so it should be possible to use such directives without editing the source code each time they need to change.
2. Define precisely what kinds of Verilog expressions are treated as "Boolean" (i.e., truth-valued) expressions within assertions, how non-Boolean values of single-bit expressions (e.g., 1'bz, 1'bx) are interpreted as Booleans, and exactly what (if any) implicit type coercion rules apply to enable non-single-bit expressions to function as Boolean expressions.
Justification:
Assertions need to be well-defined to give reliable results from one tool to another. Furthermore, the interpretation of non-Boolean values needs to be done carefully to avoid giving non-intuitive results. (For example, if the coercion from bit values to truth-values is "a==1'b1, then the assertions "always a" and "always !a" would both fail when a===1'bx.) It is important to lay a solid foundation for the temporal logic involved in assertions by defining precisely how Verilog expressions are assigned truth-values.
3. Define each assertion as an atomic object - i.e., as one statement in one location in the source code, not as a collection of statements scattered about in the source code.
Justification:
Assertions represent partial specifications that must be met by the design. Embedding assertions in the design is useful because they serve as references against which the design can be compared, and with which the design must be consistent. If an assertion is an atomic construct - possibly affected by the context in which it is contained - then it is easy to understand as reference specification. But if an assertion is dispersed in multiple places throughout the design, it becomes impossible to know whether any given assertion statement is complete, and therefore assertions lose their value as reference specifications.
4. To the extent possible, define the semantic overlap between declarative assertions and procedural assertions by specifying the equivalent (always block with embedded assertion) for each form of declarative assertion.
Justification:
System Verilog should support both declarative and procedural assertions, in order to enable the full spectrum of assertion-based verification. Defining the ways in which the two forms (declarative and procedural) are equivalent (i.e., describe exactly the same behavior) will reinforce the continuity between declarative and procedural expression of assertions and also will highlight the different capabilities each brings to the language.
5. Support description of non-overlapping, or "phased" behavior, consisting of a (possibly multi-cycle) prefix followed by a (possibly multi-cycle) suffix, such that once the prefix has occurred, then the suffix is expected, and any additional occurrences of the prefix are ignored until the suffix completes. The prefix should "match" non-deterministically - i.e., it should detect and track overlapping occurrences of the prefix until it detects a complete occurrence of the prefix. The suffix should then "match" deterministically - i.e., each successive condition in the sequence should match as soon as possible, without overlap.
Justification:
State machines often have an idle state in which they are waiting for a particular input or sequence of inputs, and that (sequence of) input(s) causes the state machine to transition to a state, starting from which it performs some preprogrammed interaction with another part of the design, finally returning to the idle state. It should be possible to reflect this "waiting to be enabled" and "enabled now and performing some task" behavior easily in an assertion. It should be noted that such state machines are easier to design if they perform one operation at a time, so single-thread execution is common, hence the need for non-overlapping (deterministic) recognition of the state machine's execution (once it is enabled).
6. Support assignment to variables as a side-effect of matching a given boolean expression in an assertion, and support reference to such variables in other parts of the same assertion.
Justification:
This ability simplifies the expression of context-sensitive assertions such as "assert that we don't have back-to-back writes to the same address", or "assert that the appropriate number of data bytes are transfered following the transfer of the byte count".
7. Support a default reset sequence specification, and implicit composition of this default reset sequence with each assertion in some region of the design.
Justification:
Having to explicitly include the reset logic in every assertion makes assertions redundant and less readable than they might be. A standard way of separately specifying the reset condition (or sequence) would allow the designer to do this once, rather than once for each assertion.
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 20:35:02 PDT