Assessment of temporal e versus requirements The assessment below considers temporal e, as defined in the LRM donated to Accellera, and a few additional features of the e language, as part of our proposal. The additional features, such as structs, local and global variables, exec statements, and spawning of objects ('new') have been used in the e versions of the examples compiled by the requirements subcommittee. If the committee selects our proposal, these extra features of the e language will be made available under the same terms as the original donation. Our justification is that the committee was originally interested in a property specification language only, whereas it now is clear that the language requirements cover a broader scope. The assessment is organized as follows: Section A lists requirements that are met by temporal e. We elaborate only if it is not straightforward to see from the language reference manual and the examples compiled by the subcommittee. Section B lists requirements that are met by temporal e, but that are deemed subjective. Section C lists requirements that temporal e supports but not in an explicit construct, leaving some programming to be done by the user. Section D lists features that are currently not supported, but could be added in principle and will be added to temporal e if selected. Finally, Section E lists requirements that are not supported and it is unclear whether they could be supported and to what end. A. Requirements met by temporal e --------------------------------- A.1 Expressiveness R1a The language must define a temporal layer. R1e The language must define more than one language binding. R2a The language must define how Verilog expressions may be used in its statements. R7a The language must allow use of boolean types. R7b The language must allow use of enumeration types. R7c The language must allow use of array/vector types. R7d The language must allow use of structure/class types. R7e The language must allow use of integer types. R7f The language must allow use of integer types >32 bits. R8a The language must allow use of standard integer arithmetic operations (+,-,*,/,mod,rem)." R8b The language must allow use of standard logical operations (=,/=,<,<=,>=)." R8c The language must allow use of standard vector operations (indexing, slicing, " concatenation). R10a The language must allow use of no-delay, no-side-effect functions in expressions." A.2 Sequences (temporal) R13a The language must allow description of repeated finite sequences of behavior. R14a The language must allow description of finite sequences. R14b The language must allow description of finite sequences with time windows. R16a The language must allow description/recognition of the first occurrence of an event. R17a The language must allow description/recognition of all occurrences of an event. R18a The language must allow description/recognition of overlapping occurrences of a given sequence. R18b The language must allow description/recognition of overlapping occurrences of two different sequences. R19a The language must allow description/recognition of the or of two finite sequences. R20a The language must allow description/recognition of the and of two finite sequences. R21a The language must allow a triggering event to be sequential, not just boolean." R23a The language must support liveness properties. R25a The language must allow arbitrary composition of formulae and temporal operators. R27a The language must be defined such that properties are closed under negation. E temporal expressions are closed under fail() which is similar to negation. R28a The language must support finite-time reasoning for static verification. Due to linear time model. R28b The language must support finite-time reasoning for simulation. Implemented in Specman. A.3 Clocks The sampling construct in temporal e allows any named event to be used as a clock. R34a The language must support description/use of level-sensitive clocks. R34b The language must support description/use of after-rising-edge clocks. R34c The language must support description/use of after-falling-edge clocks. R34d The language must support description/use of after-any-edge clocks. R35b The language must support description/use of strong clocks. R36a The language must support description/use of multiple related clocks. R36b The language must support description/use of multiple unrelated clocks. R36c The language must support description/recognition of a single behavior that involves multiple related clocks. R36d The language must support description/recognition of a single behavior that involves multiple unrelated clocks. R37a The language must support definition of abstract clocks that tick when a given sequence occurs. R37b The language must support use of abstract clocks anywhere any other clocks can be used. A.4. Resets None A.5 Meta-Language Requirements R49a The language must support definition of a block representing a nested scope. R49b The language must support declaration of local variables within a nested scope. R49c The language must support instantiation of an assertion definition within a nested scope. R49d The language must support global variables. Temporal e supports R49a-49d via structs. R51b The language must support parameterization of signal names with iteration indices. R53a The language must support a shorthand notation for specifying rising/falling signal transitions. A.6 Validation Requirements R55a The language semantics for formal verification must be well-defined. R56a The language semantics for simulation must be well-defined. R58a The language must be demonstrably formally verifiable via model checking (i.e., some path " must exist from the language into a formal model checker). We have developed compilers that compiles temporal e into automata for model checking with SMV and FormalCheck; we are collaborating with partners create a path to model checking with RuleBase. R59a The language must be demonstrably simulatable (i.e., some path must exist from the " language into a simulator). Specman does this. R68a The language must support hierarchical verification, in which a given property is first " "assumed (e.g., as an interface constraint) and then later proven." Any temporal expression can be used as an assumption (keyword assume) and as an assertion (keyword expect). A.7 Other R44a The language must include constructs that support design/environment modeling. R70a The language must support the definition of properties (to be proven). R70b The language must support the definition of constraints (assumptions). R70c The language must support the definition of events (sequences). R71a The language must support assumptions with proof obligation (e.g., interface constraints)." R71b The language must support assumptions with no proof obligation (e.g., for case splitting)." R71c The language must support formulae (to be assumed) that can specify any omega-regular language. R71d The language must support formulae (to be checked) that can specify any omega-regular language. We are convinced that temporal e has omega-regular expressiveness, though no formal proof has been published. R71e The language must support asserting every assumption. R71f The language must support assuming every assertion. R71g The meaning of a given formula must be the same, regardless of whether it is assumed or " asserted. B. Subjective requirements met by temporal e -------------------------------------------- Our installed user base -- thousands of users in hundreds of companies -- shows that temporal e meets the requirements in this section. R22 The language must support a rich set of safety properties. (Subjective) R26a The language must be easy for designers to learn. (Subjective) R55b The language semantics for formal verification must be intuitive. Subjective R56b The language semantics for simulation must be intuitive. Subjective R64a The language must be compilable with reasonable complexity. (Subjective) R65a The language must support efficient negation/complementation of properties. (Subjective) e Temporal expressions are extensively used by almost all of our customers. There was never a case of an expression that caused time/space explosion during compilation. R72a The language must introduce a minimal number of concepts. (Subjective) R73a The language must be small and simple to use. (Subjective) R74a The language must be easy to learn, write, and read. (Subjective)" C. Requirements supported via explicit programming -------------------------------------------------- Temporal e does not provide explicit constructs for these features, but they are supported via programming by the user. R9a The language must allow reference to values of objects in the design at a fixed number of cycles in the past. Example: abus1: uint(bits:16); on clk { abus1 = abus; }; R31a The language must support the recognition of multiple, concurrent (overlapping), " data-dependent instances of the same behavior described by a single property. Example property 71: event frame_f is fall(frame_) exec{ tag = bustag; } ; event spawn is { @frame_f; {[..]*true(!frame_);true(!stop) } } exec { enable = c_be[3:0] } ; on spawn { new Checker with {.tag = tag; .enable = enable;}; }; struct Checker { tag : uint(bits:70); enable : uint(bits:4); event disc is { @frame_f and true(bus_tag==tag); { [..]*true(!frame);true(!stop) } }; event compl is { @frame_f and true(bus_tag==tag); { [..]*true(!frame); true(!trdy) } }; expect p71 is [20] * {[..] * (fail @compl); @disc} => true(retry_error); }; R32d The language must support a vacuity check. Temporal e supports vacuity checking, but e-based tools, such as Specman, currently do not support it. To check if a property is not satisfied vacuously, we need to relate the its antecedent subexpressions to states of its automaton, and check if these states are reachable. R50a The language must support instance-specific application of properties. Supported via computed names, as in: struct foo { signal :string; // signal get different name per instance event mysig is rise('(signal).bar')@any; }; R51a The language must support bounded iteration over a constant range known at compile time. See property 11, or: struct LineChecker { !addr: uint(bits:4); expect rise('line_(addr).req') => { [0..7]; rise('line_(addr).ack') }; }; for a from 0 to 15 do { new AddrLine with {.addr = a;}; }; R52a The language must support specification that a signal is constant between successive "events (e.g., clock edges)." R52b The language must support specification that a signal is constant for some number of cycles. To express that ack is constant for 2 cycle of @clk: [2]*(fail (change (ack) @sys.any)) @clk; D. Features that will be added to temporal e if selected (currently not supported.) ------------------------------------------------------------------------------------ R12b If the language includes features that are useful only for formal verification or only for "simulation, then the language must define a mechanism to mark relevant usage of such " features. We will extend temporal e to meet this requirement via the proposed named sub-formulae enhancement.. R35a The language must support description/use of weak clocks. Clocks in temporal e are strong. We will extend temporal e with weak clocks. R39a The language must support selective inhibition of assertion checking during reset and/or "re-sync, in simulation." This reset feature requires monitoring a signal that is asynchronous to the given assertion. Events already provide such a mechanism. We will extend temporal e with resets. R39b The language must support selective inhibition of assertion checking during reset and/or "re-sync, in formal verification." See R39a. R45a The language must support the definition of named assertions (/sub-rules/properties). Temporal e currently supports named events, assertions, and constraints. We will add named sub-formulae to e. R45b The language must support composition of assertions to form more complex assertions. Temporal e currently supports compositions of assertions via events only. We will extend temporal e to allow composition in terms of sub formulae as well. See also R45a. R46a The language must support user-defined parameterized macro definition and expansion. Temporal e has a powerful macro facility; if selected we could include this facility in the donation. R47a The language must support definition of parameterized assertions. We will extend temporal e to meet this requirement. E. Requirements not met by temporal e ------------------------------------- R16b The language must allow description/recognition of subsequent occurrences of an event. We interpret this requirement as stating that all occurrences, except for the first occurrence of an event is to be recognized (in contrast with R16a, R17a). We don't understand the need for this and temporal e does not support it.