Subject: Assertion Requirements and Sugar 2.0
From: Erich Marschner (erichm@cadence.com)
Date: Tue Jul 09 2002 - 09:06:17 PDT
David,
It is my understanding that Vassilios has agreed that any extensions to System Verilog in the area of declarative assertions must be compatible with Sugar 2.0, the language selected to be the Accellera Formal Property Specification Language, wherever that is possible. I would like to suggest that we formally adopt this policy in the System Verilog Assertions subcommittee.
In support of this suggestion, I would like to comment on how Sugar 2.0 relates to the requirements and guidelines suggested by Steve Meier:
R1: add declarative form of assertions with ability to define sequences, time windows, implication
Sugar 2.0 supports all of the above, including extensive support for expressing sequences as extended regular expressions, logical combinations of sequences (including implication), and various forms of bounded windows (including time bounds) during which a property must hold.
R2: support directives to guide tool interpretation of assertion ( in OVA = assert, forbid, assume)
Sugar 2.0 supports all of the above, including directives 'assert', 'assume', 'restrict', and even 'cover' (which is useful in simulation coverage analysis).
R3: support synchronous clocking for R1
Sugar 2.0 supports synchronous clocking of properties (assertions and assumptions, etc.).
R4: support set/reset of assertions for R1
Sugar 2.0 supports set/reset of assertions through nesting of one property within another. The 'abort' operator is of particular use in this regard.
R5: support template definition and instantiation feature for assertions
Sugar 2.0 supports parameterized definition and instantiation of both properties (assertions) and sequences.
R6: support features for matching (first_match), restricting length (length)
Sugar 2.0 does not suppot first-match semantics at present. The addition of first-match semantics was considered but rejected, because it gave non-intuitive results. This could be revisited.
Sugar 2.0 supports restricting the length of a sequence by requiring that it complete within a given time period.
R7: support R1 in-lined within SystemVerilog code
Sugar 2.0 is defined as a separate language from Verilog, because we (the FVTC) did not have a charter to modify Verilog. However, Sugar 2.0 was intended from the start to be embeddable within Verilog, and it is appropriate to make that the next step in the evolution of Sugar 2.0.
M1: use Verilog syntax
Sugar 2.0 uses Verilog syntax wherever possible. It is defined in four layers: Boolean, Temporal, Verification, and Modeling. The Boolean layer consists of Verilog expressions. The Temporal Layer adds syntax for expressing sequences and properties - and we've made every attempt to make this additional syntax consistent with Verilog. (For example, Sugar 2.0 will support range specifications using Verilog min:max notation.) The Verification Layer adds the verification directives required above. The Modeling layer uses Verilog for modeling the environment.
M2: support SystemVerilog language features
It is not clear what this is supposed to mean, but in any case it has been the intent to make Sugar 2.0 compatible with Verilog, and with Verilog extensions being developed in the System Verilog committee.
M3: intuitive and easy to use language
Sugar 2.0 is based on Sugar 1.0, which has been used extensively at IBM and elsewhere for both simulation and formal verification, and then has been adapted to be consistent with Verilog. The widespread use of Sugar 1.0 demonstrates that the base was intuitive and easy to use, and the adaptation to Verilog can only reinforce that.
Regards,
Erich
-------------------------------------------
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 : Tue Jul 09 2002 - 09:08:18 PDT