| Rev 0.9 | |||||
| Category | Requirement | Comment/Justification | ID | Requestor | Email Date |
| Compatability | Pass/fail statement in declarative assertions | AK1 | Adam Krolnik | 7/11/02 5:43pm | |
| Compatability | Common sequence Syntax for procedural and declarative assertions | AK2 | Adam Krolnik | 7/11/02 5:43pm | |
| Operations | $posedge, $negedge, $stable | FVTC R53a Built-in functions that look at current and previous sampled value of a signal |
AK3 | Adam Krolnik | 7/31/02 6:11pm |
| Operations | Extend 3.0 system functions to multi args variable-length argument lists |
$onehot, $onecold, $isunknown make '{}' optional |
AK4 | Adam Krolnik | 7/31/02 6:11pm |
| Operations | Functionality to get previous value of signals | constant number of cycles explicit enable event |
AK5 | Adam Krolnik | 7/24/2002 |
| Semantics | Assertions executed at end of timestep | assert_strobe semantics by default for both procedural and declarative semantics | AK6 | Adam Krolnik | 7/11/02 5:43pm |
| Semantics | Automatically prevent false-firing in comb. Blocks | AK: to distribute examples for both same-time step and multiple time step | AK7 | Adam Krolnik | 7/11/02 5:43pm |
| Semantics | Formally defined semantics for assertions | Formal semantics for Formal analysis As formal as possible for simulation |
AK8 | Adam Krolnik | 7/31/02 6:11pm |
| Semantics | Simulation semantics consistent with formal | FVTC R55a-b, R56a-b As long as there is a sampling event Define subset (coding guidelines) for which semantics will be consistent. |
AK9 | Adam Krolnik | 7/31/02 6:11pm |
| Sequences | fifo semantics for handshake protocol of two expressions | FVTC R18a-b | AK10 | Adam Krolnik | 7/11/02 5:43pm |
| Usage | Declarative assertions in modules/interfaces | AK11 | Adam Krolnik | 7/11/02 5:43pm | |
| Usage | Ability to disable non-simulation properties | attribute and/or `ifdef | AK12 | Adam Krolnik | 7/11/02 5:43pm |
| Usage | Global clock specification w/ local override | Requires definition of scoping rules | AK13 | Adam Krolnik | 7/11/02 5:43pm |
| Usage | Mandatory user-specified names for assertions | AK14 | Adam Krolnik | 7/11/02 5:43pm | |
| Semantics | fifo semantics for handshake protocol of two sequences | AK15 | Adam Krolnik | ||
| Compatability | Compatible semantics & syntax with Verilog flavor of Sugar | Different semantics require different syntax Common syntax requires equivalent semantics |
CE1 | Cindy Eisner | 7/17/02 12:07pm |
| Semantics | Formally defined semantics for assertions | CE2 | Cindy Eisner | 7/17/02 12:07pm | |
| Semantics | Indentical semantics for all forms of verification | CE3 | Cindy Eisner | 7/17/02 12:07pm | |
| Semantics | Semantics independent of implementation | The interface between assertions and the rest of the code must be clearly defined | CE4 | Cindy Eisner | 7/17/02 12:07pm |
| Usage | Assertion evaluation shall have no side effects | Unless the expressions themselves have side effects | CE5 | Cindy Eisner | 7/17/02 12:07pm |
| Compatability | Be a superset of SystemVerilog 3.0 assertions | DG1 | DWG | ||
| Compatability | Uniformity of expressiveness across multiple layers of behavioral specification | procedural -> declarative -> temporal -> ?? | DG2 | DWG | |
| Operations | Capability for Dynamic disabling of assertions | suspend during reset FVTC R39a-b |
DG3 | DWG | 7/31/02 2:52pm |
| Operations | boolean cond to change value exactly once within window | DG4 | DWG | ||
| Usage | set/reset of assertions from outside the assertion via hierarchical name | Contradicts Us17 Within the same module |
DG5 | DWG | |
| Usage | Mandatory specifier for assume/check/etc | DG6 | DWG | ||
| Usage | No mechanism to specify assume/check/etc | DG7 | DWG | ||
| Usage | Ability to assert that a sequence/expression doesn't occur | if (cond) never (sequence) | DG8 | DWG | |
| Operations | Allow composition of formalae with Temporal operators | before, until, etc. | DG9 | DWG | |
| Sequences | Construct sequences from boolean conditions that are evaluated on different events | DG10 | DWG | ||
| Sequences | Construct sequences from boolean conditions that are evaluated on the same event | DG11 | DWG | ||
| Sequences | step control specified as completion of a sequence | DG12 | DWG | ||
| Operations | Define boolean behavior of 4-state, multi-bit expressions | EM1 | Erich Marschner | 7/31/02 11:33pm | |
| Operations | multi-cycle prefix w/ multi-cycle suffix Deterministic state machine with non-overlapping semantics |
prefix non-deterministic suffix deterministic |
EM2 | Erich Marschner | 7/31/02 11:33pm |
| Operations | Allow assignment/reference to variables within an assertion | Implementation may be difficult | EM3 | Erich Marschner | 7/31/02 11:33pm |
| Semantics | Define semantic overlap between declarative and procedural assertions | EM4 | Erich Marschner | 7/31/02 11:33pm | |
| Usage | Mechanism to name assertions | Optional name | EM5 | Erich Marschner | |
| Usage | Assertions as atomic objects | #REF! | EM6 | Erich Marschner | 7/31/02 11:33pm |
| Usage | Default reset for assertions in given region | EM7 | Erich Marschner | 7/31/02 11:33pm | |
| Usage | Optional specifier for assume/check/etc | FVTC R71e-f | EM8 | Erich Marschner | 7/31/02 11:33pm |
| Operations | Recognition of first occurence of an event | FVTC R16a-b, R17a Sugar does not meet this req. |
FV1 | FVTC (via EM) | 7/26/02 8:26pm |
| Operations | Recognition of all occurences of an event | FVTC R16a-b, R17a | FV2 | FVTC (via EM) | 7/26/02 8:26pm |
| Operations | Support Safety and Liveness properties | FVTC R22, 23a | FV3 | FVTC (via EM) | 7/26/02 8:26pm |
| Semantics | Finite Time Reasoning | FVTC R28a-b Explicitly NOT Infinite Time Reasoning |
FV4 | FVTC (via EM) | 7/26/02 8:26pm |
| Semantics | Closed under negation of a formula, not sequences | FVTC R27a Requires composition of formulae |
FV5 | FVTC (via EM) | 7/26/02 8:26pm |
| Sequences | Repeated Sequences | FVTC R13a DAS: *[n:m] |
FV6 | FVTC (via EM) | 7/26/02 8:26pm |
| Usage | Recognition of multiple, concurrent (overlapping) data-dependent instances of the same behavior described by a single property | FVTC R31a Same as Templates? |
FV7 | FVTC (via EM) | 7/26/02 8:26pm |
| Usage | Vacuity Check | FVTC R32d | FV8 | FVTC (via EM) | 7/26/02 8:26pm |
| Usage | Support for Weak and Strong clocks | FVTC R35a-b | FV9 | FVTC (via EM) | 7/26/02 8:26pm |
| Usage | Level-sensitive clocks | FVTC R34a | FV10 | FVTC (via EM) | 7/26/02 8:26pm |
| Usage | Define standard method to separate design code from verification code | PN1 | Prakash Narain | ||
| Compatability | Assertion syntax compatible with SystemVerilog | Same as C5 | RR1 | Rajeev Ranjan | 7/25/02 12:35am |
| Operations | refer to future values of signal | RR2 | Rajeev Ranjan | 7/25/02 12:35am | |
| Operations | refer to past values of signal | Compile-time constant. When in the timeslot is the value taken? |
RR3 | Rajeev Ranjan | 7/25/02 12:35am |
| Operations | Keyword-based specification of common relationships | mutex,inset,posedge,etc. | RR4 | Rajeev Ranjan | 7/25/02 12:35am |
| Operations | boolean cond to occur within window | RR5 | Rajeev Ranjan | 7/25/02 12:35am | |
| Operations | boolean cond to occur throughout window | RR6 | Rajeev Ranjan | 7/25/02 12:35am | |
| Operations | boolean cond to hold value throughout window | FVTC R52a-b | RR7 | Rajeev Ranjan | 7/25/02 12:35am |
| Operations | boolean cond to change value within window | Must change at least once. No implication on what happens after the first change. | RR8 | Rajeev Ranjan | 7/25/02 12:35am |
| Semantics | Cycle-based semantics | Presence of #delays should be ignored Same as Sm1, but for procedural as well Sampling and sequence stepping should be triggered by an event on a signal or expression |
RR9 | Rajeev Ranjan | 7/25/02 12:35am |
| Sequences | sequence completion to trigger other operations | FVTC R21a, R37a First occurence of sequence only |
RR10 | Rajeev Ranjan | 7/25/02 12:35am |
| Sequences | time-based temporal windows | FVTC R14b Defined by cycle count |
RR11 | Rajeev Ranjan | 7/25/02 12:35am |
| Sequences | event-based temporal windows | RR12 | Rajeev Ranjan | 7/25/02 12:35am | |
| Sequences | sequence completion for coverage | RR13 | Rajeev Ranjan | 7/25/02 12:35am | |
| Usage | Procedural assertions | RR14 | Rajeev Ranjan | 7/25/02 12:35am | |
| Usage | Mandatory unique name for assertions | User-specified name. Unique within a scope | RR15 | Rajeev Ranjan | 7/25/02 12:35am |
| Usage | set/reset of assertions from outside the assertion | Contradicts Us17 Within the same module |
RR16 | Rajeev Ranjan | 7/25/02 12:35am |
| Usage | Optional specifier for assume/check/etc | RR17 | Rajeev Ranjan | 7/25/02 12:35am | |
| Usage | Easy to use | FVTC R26a | RR18 | Rajeev Ranjan | 7/25/02 12:35am |
| Operations | distinct method for Dynamic disabling of assertions | suspend during reset FVTC R39a-b |
RH1 | Richard Ho | 7/31/02 2:52pm |
| Semantics | Synchronous assertions | implied,default or explicit clock Clarification: Only synchronous assertions? |
RH2 | Richard Ho | 7/31/02 2:52pm |
| Usage | Procedural assertions | RH3 | Richard Ho | 7/31/02 2:52pm | |
| Usage | Inference from context for variable values | RH4 | Richard Ho | 7/31/02 2:52pm | |
| Usage | Ability to set severity of assertions | RH5 | Richard Ho | 7/31/02 2:52pm | |
| Usage | Support verification directives | assert,assume, etc. | RH6 | Richard Ho | 7/31/02 2:52pm |
| Usage | Assertion encapsulation as library element with arguments | FVTC R45b, R46a, R47a | RH7 | Richard Ho | 7/31/02 2:52pm |
| Usage | Declarative assertion linked to module definition | RH8 | Richard Ho | 7/31/02 2:52pm | |
| Usage | Assertions have no side-effects | RH9 | Richard Ho | 7/31/02 2:52pm | |
| Compatability | support SystemVerilog language features SystemVerilog type extensions supported in assertions |
Different semantics require different syntax Common syntax requires equivalent semantics |
SM1 | Steve Meier | 7/9/02 10:43am |
| Compatability | Use SystemVerilog-compatible syntax | Different semantics require different syntax Common syntax requires equivalent semantics |
SM2 | Steve Meier | 7/9/02 10:43am |
| Sequences | Ability to define/declare reusable sequences (and refer to them by name) | SM3 | Steve Meier | 7/9/02 10:43am | |
| Sequences | Sequences with Time Windows | repetition of "true" | SM4 | Steve Meier | 7/9/02 10:43am |
| Sequences | Ability for notification of every completion of a sequence | OVA match - capability, not necessarily operator equiv. to endpoint operator in Sugar |
SM5 | Steve Meier | 7/9/02 10:43am |
| Usage | Declarative Form of Assertion | SM6 | Steve Meier | 7/9/02 10:43am | |
| Usage | Declarative assertions in-line with SystemVerilog | SM7 | Steve Meier | 7/9/02 10:43am | |
| Usage | intuitive and easy-to-use | SM8 | Steve Meier | 7/9/02 10:43am | |
| Sequences | support iff in step-control | R1.5 | SD1 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | restrict length of sequences | R6.2 OVA length |
SD3 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | assert that boolean condition is true for duration of sequence | Time window can also be while sequence is evaluated (R6.2) | SD4 | Surrendra Dudani | 7/26/02 10:56am |
| Usage | Declarative assertions external to modules | R1.6: link to module/instance FVTC R50a in $root |
SD5 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | multiple clocks and relationship between them | FVTC R36a-d Surrendra's R3 |
SD6 | Surrendra Dudani | 7/26/02 10:56am |
| Usage | Ability to group assertions with common clock | R6.3 | SD7 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to group assertions with common accept/reject | R6.3 | SD8 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Ability for notification of earliest completion of a sequence | R6.1 OVA first_match - capability, not necessarily operator No Sugar equivalent operator |
SD9 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to define sequences as regular expressions | R1.1 | SD10 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to define sample clock (simple event expression) for sequence evaluation (per-assertion) | R1.2 | SD11 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Sample clock can be any boolean expression of other signals | R3.1 | SD12 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Specify rules for sample clock to be extracted/inferred from context (same rules as synthesis) | R1.2 OK if clock cannot be inferred |
SD13 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to specify default clock for all assertions within a scope | R1.2 | SD14 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to specify default clock for all assertions globally | R1.2 | SD15 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to define sequences with relationship between events | R1.3 Ev1 happens before/after Ev2 Unspecified relationship between Ev1,Ev2 |
SD16 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Basic implication operator if (bool) then (seq1) [else (seq2)]; |
R1.4: Condition may only be boolean No circular looping |
SD17 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Explicitly disallow sequential expression implication | R1.4 | SD18 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to pause a sequence until some condition becomes true | R1.4 | SD19 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Operator to match some other sequence | returns boolean | SD20 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Operator to match some other sequence in a different clock domain | SD21 | Surrendra Dudani | 7/31/02 4:17pm | |
| Usage | Directive to mark statement as an assertion | R2.1: "check", "forbid" | SD22 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Directive to mark statement as constraint | R2.2: "assume" | SD23 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Directive to indicate statement may be either an assertion or a constraint | R2.3 | SD24 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to define multiple sample clocks for different sequences | R3.2 | SD25 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to refer to and/or synchronize between sequences with different sample clocks | R3.2 | SD26 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to specify explicit synchronous condition to force sequence to terminate as "successful" | R4.1 | SD27 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to specify explicit synchronous condition to force sequence to terminate as "failed" | R4.2 | SD28 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to specify explicit asynchronous event to force sequence to terminate as "successful" | R4.3 | SD29 | Surrendra Dudani | 7/31/02 4:17pm |
| Sequences | Ability to specify explicit asynchronous event to force sequence to terminate as "failed" | R4.4 | SD30 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to define pre-built assertion template | R5 | SD31 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to instantiate template as a macro | R5: No additional hierarchy | SD32 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to instantiate template | R5: template formals continually get values of actual signals (pass-by-reference) | SD33 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Specify that sequence hold true during time window | R6.2 | SD34 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Ability to operate on compile-time constant sets | R6.4 | SD35 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Ability to operate on dynamic-sized sets | R6.4 | SD36 | Surrendra Dudani | 7/31/02 4:17pm |
| Semantics | Clocked sequential assertion construct defined to have consistent semantics between event-based simulation and cycle-based formal evaluation | R7.1 | SD37 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Restrict sequential assertions from being used in combinational always blocks | R9.1 | SD38 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Automatically extract/infer reset condition from usage context | R10.3 | SD39 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Automatically extract/infer enable condition from usage context | R10.4 | SD40 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Automatically extract/infer lhs from usage context | R10.1 | SD50 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Automatically extract/infer rhs from usage context | R10.1 | SD51 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to refer to inferred information from within template | R10.1 | SD52 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Ability to declare local variables within assertions | R11.1 | SD53 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Ability to refer to future value of a signal on the next cycle. | R11.3 | SD54 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Support automatic variables, localized to a particular execution of a given assertion | R11.4 | SD55 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Function/API to determine the status of specified named assertion(s) | R12.1 | SD56 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Function/API to determine the status of specified named sequence(s) | R12.1 | SD57 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | New coverage-specific datatype | R12.3 | SD58 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to define time window defined by assertion event | R12.2 | SD59 | Surrendra Dudani | 7/31/02 4:17pm |
| Usage | Ability to construct time windows from other time windows | R12.4 | SD60 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Function/API to record data values sampled by assertion events | R12.5 | SD61 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Function/API to support coverage of paths through a sequence | R12.6 | SD62 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Function/API to combine multiple coverage items (cross-coverage) | R12.7 | SD63 | Surrendra Dudani | 7/31/02 4:17pm |
| Operations | Function/API to exclude data items or sequences from coverage | R12.8 | SD64 | Surrendra Dudani | 7/31/02 4:17pm |
| Semantics | Define a semantic subset that can be simulated on-the-fly | TF1 | Tom Fitzpatrick | 7/30/02 5:05pm | |
| Sequences | Parameterized sequences | TF2 | Tom Fitzpatrick | 7/30/02 5:05pm | |
| Sequences | Sequences referred to by name | TF3 | Tom Fitzpatrick | 7/30/02 5:05pm | |
| Sequences | Combine sequences | &&, etc. FVTC R19a, R20a |
TF4 | Tom Fitzpatrick | 7/30/02 5:05pm |
| Sequences | Compose complex sequences out of other sequences | TF5 | Tom Fitzpatrick | 7/30/02 5:05pm | |
| Usage | Encapsulate multiple sequences and instantiate | formal and actual arguments | TF6 | Tom Fitzpatrick | 7/30/02 5:05pm |
| Compatability | Assertion and sequential expression syntax compatible in style with the rest of SystemVerilog | TF7 | Tom Fitzpatrick |