| Rev 0.4 | |||||||
| Category | Number | Requirement | Comment/Justification | Requestor | Email Date | DWG | Agree |
| Compatability | C2 | Pass/fail statement in declarative assertions | Adam Krolnik | 7/11/02 5:43pm | 2 | 1 | |
| Compatability | C3 | Common sequence Syntax for procedural and declarative assertions | Adam Krolnik | 7/11/02 5:43pm | 1 | 1 | |
| Operations | Op12 | $posedge, $negedge, $stable | FVTC R53a Clarify |
Adam Krolnik | 7/31/02 6:11pm | ||
| Operations | Op13 | Extend 3.0 system functions to multi-bit args | Clarify | Adam Krolnik | 7/31/02 6:11pm | ||
| Operations | Op4 | Functionality to get previous value of signals | constant number of cycles explicit sample event |
Adam Krolnik | 7/11/02 5:43pm | 1 | 1 |
| Semantics | Sm2 | Assertions executed at end of timestep | Adam Krolnik | 7/11/02 5:43pm | |||
| Semantics | Sm3 | Automatically prevent false-firing in comb. Blocks | Adam Krolnik | 7/11/02 5:43pm | |||
| Semantics | Sm4 | Formally defined semantics for assertions | Adam Krolnik | 7/31/02 6:11pm | |||
| Semantics | Sm5 | Simulation semantics consistent with formal | FVTC R55a-b, R56a-b | Adam Krolnik | 7/31/02 6:11pm | ||
| Sequences | Sq5 | Overlapping sequences with fifo semantics | FVTC R18a-b | Adam Krolnik | 7/11/02 5:43pm | ||
| Usage | Us4 | Declarative assertions in modules/interfaces | Adam Krolnik | 7/11/02 5:43pm | |||
| Usage | Us6 | Ability to disable non-simulation properties | Adam Krolnik | 7/11/02 5:43pm | |||
| Usage | Us7 | Global clock specification w/ local override | Adam Krolnik | 7/11/02 5:43pm | |||
| Usage | Us8 | Mandatory names for assertions | Adam Krolnik | 7/11/02 5:43pm | |||
| Compatability | C3 | Compatible semantics & syntax with Verilog flavor of Sugar | Different semantics require different syntax Common syntax requires equivalent semantics |
Cindy Eisner | 7/17/02 12:07pm | 2 | 0 |
| Semantics | Sm4 | Formally defined semantics for assertions | Cindy Eisner | 7/17/02 12:07pm | |||
| Semantics | Sm5 | Semantics independent of implementation | The interface between assertions and the rest of the code must be clearly defined | Cindy Eisner | 7/17/02 12:07pm | ||
| Semantics | Sm5 | Indentical semantics for all forms of verification | Cindy Eisner | 7/17/02 12:07pm | |||
| Usage | Us9a | Assertion evaluation shall have no side effects | Unless the expressions themselves have side effects | Cindy Eisner | 7/17/02 12:07pm | ||
| Compatability | C5 | Be a superset of SystemVerilog 3.0 assertions | DWG | 2 | 1 | ||
| Compatability | C6 | Uniformity of expressiveness across multiple layers of behavioral specification | procedural -> declarative -> temporal -> ?? | DWG | 1 | 1 | |
| Operations | Op2a | Capability for Dynamic disabling of assertions | suspend during reset FVTC R39a-b |
DWG | 7/31/02 2:52pm | 1 | 1 |
| Operations | Op9a | boolean cond to change value exactly once within window | DWG | 1 | 1 | ||
| Operations | Op14 | Define boolean behavior of 4-state, multi-bit expressions | Erich Marschner | 7/31/02 11:33pm | 1 | 1 | |
| Operations | Op15 | multi-cycle prefix w/ multi-cycle suffix Deterministic state machine with non-overlapping semantics |
prefix non-deterministic suffix deterministic |
Erich Marschner | 7/31/02 11:33pm | 1 | 1 |
| Operations | Op16 | Allow assignment/reference to variables within an assertion | Implementation may be difficult | Erich Marschner | 7/31/02 11:33pm | 1 | 1 |
| Semantics | Sm8 | Define semantic overlap between declarative and procedural assertions | Erich Marschner | 7/31/02 11:33pm | |||
| Usage | Us17 | Assertions as atomic objects | Contradicts Op9a | Erich Marschner | 7/31/02 11:33pm | ||
| Usage | Us18 | Default reset for assertions in given region | Erich Marschner | 7/31/02 11:33pm | |||
| Usage | Us2 | Optional specifier for assume/check/etc | FVTC R71e-f | Erich Marschner | 7/31/02 11:33pm | ||
| Operations | Op17a | Recognition of first occurence of an event | FVTC R16a-b, R17a Sugar does not meet this req. |
FVTC (via EM) | 7/26/02 8:26pm | 2 | 0 |
| Operations | Op17b | Recognition of all occurences of an event | FVTC R16a-b, R17a | FVTC (via EM) | 7/26/02 8:26pm | 1 | 1 |
| Operations | Op18 | Support Safety and Liveness properties | FVTC R22, 23a | FVTC (via EM) | 7/26/02 8:26pm | ||
| Semantics | Sm10 | Finite Time Reasoning | FVTC R28a-b | FVTC (via EM) | 7/26/02 8:26pm | ||
| Semantics | Sm9 | Closed under negation | FVTC R27a | FVTC (via EM) | 7/26/02 8:26pm | ||
| Sequences | Sq15 | Repeated Finite Sequences | FVTC R13a | FVTC (via EM) | 7/26/02 8:26pm | ||
| Usage | Us19 | Recognition of multiple, concurrent (overlapping) data-dependent instances of the same behavior described by a single property | FVTC R31a Same as Templates? |
FVTC (via EM) | 7/26/02 8:26pm | ||
| Usage | Us20 | Vacuity Check | FVTC R32d | FVTC (via EM) | 7/26/02 8:26pm | ||
| Usage | Us21 | Support for Weak and Strong clocks | FVTC R35a-b | FVTC (via EM) | 7/26/02 8:26pm | ||
| Usage | Us22 | Level-sensitive clocks | FVTC R34a | FVTC (via EM) | 7/26/02 8:26pm | ||
| Compatability | C4 | Assertion syntax compatible with SystemVerilog | Same as C5 | Rajeev Ranjan | 7/25/02 12:35am | ||
| Operations | Op10 | refer to future values of signal | Rajeev Ranjan | 7/25/02 12:35am | 4 | 1 | |
| Operations | Op4 | refer to past values of signal | Rajeev Ranjan | 7/25/02 12:35am | |||
| Operations | Op5 | Keyword-based specification of common relationships | mutex,inset,posedge,etc. Need clarification |
Rajeev Ranjan | 7/25/02 12:35am | ||
| Operations | Op6 | boolean cond to occur within window | Rajeev Ranjan | 7/25/02 12:35am | 1 | 1 | |
| Operations | Op7 | boolean cond to occur throughout window | Rajeev Ranjan | 7/25/02 12:35am | 1 | 1 | |
| Operations | Op8 | boolean cond to hold value within/throughout window | FVTC R52a-b | Rajeev Ranjan | 7/25/02 12:35am | 1 | 1 |
| Operations | Op9 | boolean cond to change value within window | Does it change once or can it change multiple times? | Rajeev Ranjan | 7/25/02 12:35am | ||
| Semantics | Sm6 | Cycle-based semantics | Rajeev Ranjan | 7/25/02 12:35am | |||
| Sequences | Sq10 | sequence completion to trigger other operations | FVTC R21a, R37a | Rajeev Ranjan | 7/25/02 12:35am | ||
| Sequences | Sq6 | time-based temporal windows | FVTC R14b | Rajeev Ranjan | 7/25/02 12:35am | ||
| Sequences | Sq8 | event-based temporal windows | Rajeev Ranjan | 7/25/02 12:35am | |||
| Sequences | Sq9 | sequence completion for coverage | Rajeev Ranjan | 7/25/02 12:35am | |||
| Usage | Us10 | Procedural assertions | Rajeev Ranjan | 7/25/02 12:35am | |||
| Usage | Us11 | Mandatory unique name for assertions | Rajeev Ranjan | 7/25/02 12:35am | |||
| Usage | Us12 | set/reset of assertions from outside the assertion | Contradicts Us10 | Rajeev Ranjan | 7/25/02 12:35am | ||
| Usage | Us2 | Optional specifier for assume/check/etc | Rajeev Ranjan | 7/25/02 12:35am | |||
| Usage | Us5 | Easy to use | FVTC R26a | Rajeev Ranjan | 7/25/02 12:35am | ||
| Operations | Op2 | distinct method for Dynamic disabling of assertions | suspend during reset FVTC R39a-b |
Richard Ho | 7/31/02 2:52pm | 2 | 0 |
| Semantics | Sm6 | Synchronous assertions | implied,default or explicit clock | Richard Ho | 7/31/02 2:52pm | ||
| Usage | Us10 | Procedural assertions | Richard Ho | 7/31/02 2:52pm | |||
| Usage | Us15 | Inference from context for variable values | Richard Ho | 7/31/02 2:52pm | |||
| Usage | Us16 | Ability to set severity of assertions | Richard Ho | 7/31/02 2:52pm | |||
| Usage | Us2 | Support verification directives | assert,assume, etc. | Richard Ho | 7/31/02 2:52pm | ||
| Usage | Us3 | Assertion encapsulation as library element with arguments | FVTC R45b, R46a, R47a | Richard Ho | 7/31/02 2:52pm | ||
| Usage | Us4 | Declarative assertion linked to module definition | Richard Ho | 7/31/02 2:52pm | |||
| Usage | Us9 | Assertions have no side-effects | Richard Ho | 7/31/02 2:52pm | |||
| Compatability | C1 | Use SystemVerilog-compatible syntax | Different semantics require different syntax Common syntax requires equivalent semantics |
Steve Meier | 7/9/02 10:43am | 1 | 1 |
| Compatability | C1 | support SystemVerilog language features SystemVerilog type extensions supported in assertions |
Different semantics require different syntax Common syntax requires equivalent semantics |
Steve Meier | 7/9/02 10:43am | 1 | 1 |
| Operations | Op1 | Support for implication | Steve Meier | 7/9/02 10:43am | 1 | 1 | |
| Semantics | Sm1 | synchronous clocking for declarative assertions | Steve Meier | 7/9/02 10:43am | |||
| Sequences | Sq1 | Ability to define sequences | Steve Meier | 7/9/02 10:43am | |||
| Sequences | Sq2 | Sequences with Time Windows | Steve Meier | 7/9/02 10:43am | |||
| Sequences | Sq3 | ability to match sequences | OVA first_match | Steve Meier | 7/9/02 10:43am | ||
| Sequences | Sq4 | restrict length of sequences | OVA length | Steve Meier | 7/9/02 10:43am | ||
| Usage | Us1 | Declarative Form of Assertion | Steve Meier | 7/9/02 10:43am | |||
| Usage | Us2 | Guide tool interpretation | assert,check,assume,etc. | Steve Meier | 7/9/02 10:43am | ||
| Usage | Us3 | template definition and instantiation of assertions | Steve Meier | 7/9/02 10:43am | |||
| Usage | Us4 | Declarative assertions in-line with SystemVerilog | Steve Meier | 7/9/02 10:43am | |||
| Usage | Us5 | intuitive and easy-to-use | Steve Meier | 7/9/02 10:43am | |||
| Operations | Op3a | asynchronous form of distinct pass/fail method | Surrendra Dudani | 7/26/02 10:56am | |||
| Sequences | Sq11 | support iff in step-control | Surrendra Dudani | 7/26/02 10:56am | |||
| Sequences | Sq12 | step control specified as expression of design signals | Surrendra Dudani | 7/26/02 10:56am | |||
| Sequences | Sq7 | assert the sequence is true for duration of time window | Surrendra Dudani | 7/26/02 10:56am | |||
| Sequences | Sq8 | define sequences with relationship between events | Surrendra Dudani | 7/26/02 10:56am | |||
| Usage | Us1 | Declarative assertions external to modules | link to module/instance FVTC R50a |
Surrendra Dudani | 7/26/02 10:56am | ||
| Usage | Us13 | multiple clocks and relationship between them | FVTC R36a-d | Surrendra Dudani | 7/26/02 10:56am | ||
| Usage | Us14 | Ability to group assertions with common clock | Surrendra Dudani | 7/26/02 10:56am | |||
| Semantics | Sm7 | Semantic subset for simulation on-the-fly | Tom Fitzpatrick | 7/30/02 5:05pm | |||
| Sequences | Sq1 | Sequences referred to by name | Tom Fitzpatrick | 7/30/02 5:05pm | |||
| Sequences | Sq1 | Parameterized sequences | Tom Fitzpatrick | 7/30/02 5:05pm | |||
| Sequences | Sq13 | Combine sequences | &&, etc. FVTC R19a, R20a |
Tom Fitzpatrick | 7/30/02 5:05pm | ||
| Sequences | Sq14 | Compose complex sequences out of other sequences | Tom Fitzpatrick | 7/30/02 5:05pm | |||
| Usage | Us3 | Encapsulate multiple sequences and instantiate | formal and actual arguments | Tom Fitzpatrick | 7/30/02 5:05pm |