| Anonymous | Login | 2010-09-03 01:59 PDT |
| Main | My View | View Issues | Docs | Wiki |
| Viewing Issue Simple Details [ Jump to Notes ] [ Wiki ] | [ View Advanced ] [ Issue History ] [ Print ] | ||||||
| ID | Category | Severity | Date Submitted | Last Update | |||
| 0002398 | [SystemVerilog P1800] SV-SC | major | 2008-05-27 16:07 | 2008-12-19 17:59 | |||
| Reporter | Erik_Seligman | View Status | public | ||||
| Assigned To | Erik_Seligman | ||||||
| Priority | high | Resolution | fixed | ||||
| Status | closed | Product Version | P1800-2008/D5 | ||||
| Summary | 0002398: More consistent semantics for concurrent assertions in procedural code | ||||||
| Description |
In SV-SC we have reviewed the definitions of concurrent assertion behavior in procedural code. The currently existing defs, in there since the 2005 standard, are problematic in many ways, as they allow these assertions but do not keep their behavior consistent with the procedures in which they appear. This has resulted in the need for bolted-on patches for features like concurrent asserts in loops (1995) and $inferred_enable (in proposal 1674). There was significant concern about building future features like checkers over this rickety framework. We believe we have a redesign of this feature that is cleaner, mostly backwards compatible, and inherently supports nearly all procedural constructs, including loops, without needing extra proposals. It even allows for a natural extension to tasks and functions in a future proposal, something nearly impossible in the current definition. |
||||||
| Additional Information | (written proposal to be posted later this week) | ||||||
| Tags | No tags attached. | ||||||
| Type | Enhancement | ||||||
| Attached Files |
 concurrent_procedural_es080717b.doc [^] (239,104 bytes) 2008-07-18 10:05 concurrent_procedural_es080717b.pdf [^] (133,542 bytes) 2008-07-18 10:06 concurrent_procedural_es080721.doc [^] (239,104 bytes) 2008-07-21 09:44 concurrent_procedural_es080721.pdf [^] (177,655 bytes) 2008-07-21 09:45 concurrent_procedural_es080722.doc [^] (238,080 bytes) 2008-07-22 07:44 concurrent_procedural_es080722.pdf [^] (133,864 bytes) 2008-07-22 07:44 concurrent_procedural_es080723.doc [^] (237,568 bytes) 2008-07-23 09:31 concurrent_procedural_es080723.pdf [^] (133,900 bytes) 2008-07-23 09:31 concurrent_procedural_es080801.pdf [^] (134,025 bytes) 2008-08-01 12:12 concurrent_procedural_es080801.doc [^] (240,128 bytes) 2008-08-01 12:13 concurrent_procedural_es080801b.pdf [^] (134,561 bytes) 2008-08-01 15:32 concurrent_procedural_es080801b.doc [^] (247,808 bytes) 2008-08-01 15:32 concurrent_procedural_es080803.doc [^] (249,344 bytes) 2008-08-03 13:19 concurrent_procedural_es080803.pdf [^] (134,597 bytes) 2008-08-03 13:19 concurrent_procedural_es080804.pdf [^] (140,851 bytes) 2008-08-04 10:19 concurrent_procedural_es080804.doc [^] (248,832 bytes) 2008-08-04 10:20 concurrent_procedural_es080811b.pdf [^] (135,554 bytes) 2008-08-11 09:19 concurrent_procedural_es080811b.doc [^] (241,152 bytes) 2008-08-11 09:20 concurrent_procedural_es080813.doc [^] (241,152 bytes) 2008-08-13 15:23 concurrent_procedural_es080813.pdf [^] (135,672 bytes) 2008-08-13 15:24 |
||||||
|
|
|||||||
 Relationships |
||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
|
Notes |
|
 (0007255)Erik_Seligman (developer) 2008-07-23 09:33 |
Passed by voice vote at SV-SC meeting 2008-07-22, conditional on minor edit implemented in version posted by Erik Seligman on 2008-07-23. 12y/0n/0a |
|
(0007275) Erik_Seligman (developer) 2008-08-01 12:12 |
Changing to 'feedback' so I can edit based on Champion requests. |
 (0007277)Neil Korpusik (administrator) 2008-08-01 18:22 edited on: 2008-08-05 11:02 |
The proposal was unanimously approved by the Champions in the July 31st, 2008 conference call with the following friendly amendments. a. This proposal (page 2, top paragraph) strikes the text that says that assertion local variables use current values, not Preponed values. This creates an inconsistency between Clause 16 and Annex F. Local variables do not and have never used Preponed values. The text that provides an exception for local variables should be restored. Why does it refer to "automatic values" instead of "automatic variables"? John provided the following rewording: "All variables in a concurrent assertion use the value sampled in the Preponed region of a time slot with the exception of local variables, constant casts and automatic variables in procedural code (see 16.15.5), and free checker variables (see 17.6.2)." This same change should be made in other places (with or without the checker variable phrase). b. The language discussing the beginning of evaluation of a matured assertion should reference the "leading clocking event" rather than just the "clocking event" of the assertion. 16.15.5, last paragraph, for multiple clocked assertions we talk about the "leading clock event". 3 places need to be changed c. "assertions's" --> "assertion's" d. Page 8, 16.15.5.1, first example, 1st paragraph after the example For the first pass through there is an issue. Add text to say, "assuming that posedge clk" doesn't occur at time 0. Could also show the clock oscillator definition and write it to not allow the corner case. Static variable initialization is the same as performing the assignment in an initial procedure. Correction: this last statement is not correct. Below is the text copied from 10.5 of draft 6. This is a change from what was in 1364 [Neil] "Setting the initial value of a static variable as part of the variable declaration (including static class members) shall occur before any initial or always procedures are started." e. 16.15.5, page 3, first new paragraph, in the middle, "Each of these entries" --> "Each of the entries in this queue" f. 16.15.5, page 3, 2nd new paragraph The definition of "mature" is given on the second usage. It would be best to define it the first time the term is used. g. 16.15.5, page 3, last paragraph, 4th line, "an attempt" --> "an evaluation attempt" This change is required in two places. Evaluation attempt is used elsewhere, they should all be consistent in the proposal. h. page 4, example for p1, and the text in first paragraph. "If no clock can be inferred from the procedural context, then the clocks shall be inferred from the current scope as if the assertion were instantiated immediately before the procedure." Then the only other way to pick up a clock is default clocking. Should it just say to use default clocking? This seems to be worded in an odd way. i. Page 8, 16.15.5.1, the tick is going the wrong way (several) j. Page 9, last paragraph before 3rd example, 3rd line, "which shall not be modified" --> "that shall not be modified" k. Page 10, last paragraph, 16.15.5.1, found this to be confusing. Inferred enabling conditions no longer exist in this version. New people will attempt to understand this in terms of 1800-2009. If there is no discussion on inferred enabling conditions, they will have troubling understanding it. It might be more appropriate to make this a note. It should also refer to a particular clause in the 2005 standard. l. 6.24.1, doesn't like the placement of this. Prefers to move this paragraph earlier or later. Before the 2 line paragraph "when casting to a pre-defined type" would be better. |
|
(0007298) Erik_Seligman (developer) 2008-08-05 09:37 |
SV-SC voted to approve latest edits at 2008-08-05 mtg. 9y/0n/0a. |
|
(0007321) Erik_Seligman (developer) 2008-08-11 09:04 |
Needed to make a few additional minor edits from Champions. |
|
(0007351) Neil Korpusik (administrator) 2008-08-18 16:56 |
The following issues were noted in the Champions conference call held on August 7th, 2008. This proposal was not on the agenda and was not voted on during the meeting, but these issues were noted during the discussion. 1. page 8, example, the declaration assignment needs to be added back in. Otherwise, the value of the variable is not right, when the first pass of the loop occurs at a time other than time 0. 2. page 2, in the "else portion" of the text It shouldn't be talking about free checker variables. Note: this set of changes is included in the proposal uploaded on August 11. |
|
(0007388) Erik_Seligman (developer) 2008-08-21 10:35 |
Final edits approved in SV-SC voice vote, 8/19/08. |
|
(0007390) Neil Korpusik (administrator) 2008-08-23 09:27 |
The proposal was unanimously approved by the Champions in the August 21st, 2008 conference call. |
|
(0007401) Neil Korpusik (administrator) 2008-08-28 09:22 |
The proposal was unanimously approved by the Working Group in the continuation of the August 14, 2008 conference call, which was held on August 28, 2008. |
 (0007499)Stuart Sutherland (manager) 2008-09-11 05:43 |
The change proposal was implemented in draft 7. |
|
(0007521) Erik_Seligman (developer) 2008-09-15 09:22 |
I reviewed Draft 7, and spotted the following implementation issues: 1. 20.11, p.533, top: "pending procedural assertion instance (see 16.5.6)". Instance should be plural here: "pending procedural assertion instances". 2. Annex F.2, p. 1152, text fragment between two examples: "is transformed ... the assertion": The word 'into' should have been retained here rather than struck for this sentence to make sense. 3. Incorrect references in right margin to 1938 instead of 2398: p. 553, 1045, 170, 1151, 1152, 1159 4. 16.5, p.315, top: The paragraph at the top, "The values of variables... (RTL) description", has an editorial note "Is this cross reference correct?" In fact it isn't-- it's referring to proposal 1995, our original proposal to enable looped concurrent assertions, which was superseded by the more general 2398. Furthermore, since this paragraph is redundant with the following one ("All variables in a concurrent assertion...") which was introduced by 2398, I think only the one in 2398 should be kept. Thus, we should delete this top paragraph on p.315. I'm not sure if some proposal along the way was thought to have struck it, or if this was an oversight... tell me if you think we need to handle this as a new Mantis item, or can delete the redundant paragraph editorially at this stage. |
 (0007525)gordonv (developer) 2008-09-16 10:13 |
Gord's additional comments: 1) In 16.5.6.4, "The disable statement" the word "disable" is a keyword 2) In 16.15.7, the first sentence "The following elaboration ... and disable expression." should probably terminate with a colon rather than a period. That was missed in the original proposal too. |
|
(0007544) Erik_Seligman (developer) 2008-09-22 09:49 |
One more change needed. SV-AC noticed a part at the end of section 16.16 (p. 417 of Draft 7) that reads: ------------------------- // Only enable condition and clocking event are inferred from an always // block always procedure. Assertion a8 is equivalent to // assert property (@(posedge clk) !bit'(rst!='b0) |-> (a |=> b)); always @(posedge clk or posedge rst) if (rst) ... else begin a8 : assert property (a |=> b); ... end endmodule In assertion a8 the inferred enabling condition is from the else clause of the if-else statement, and thus it has to represent the complementary interpretation of the four-valued expression in the if condition. One such form is as indicated in the comment above a8. Other equivalent forms may be used, such as ((rst !='b0) !== 1'b1). ------------------------------- Since this proposal eliminated the inferred enabling condition, all the text quoted above (the final section of the example + the paragraph below) needs to be removed, and replaced with a simple 'endmodule' to end the example. Tell me if we need a Mantis for this or can do it editorially. |
 (0007558)Lisa Piper (developer) 2008-09-30 13:17 |
I have one more thing in addition to the previous three comments. The following text is in accordance with the proposal, however the reference to the section from the IEEE 2005 section should be 17.13, not 16.14. "NOTE--- this is an area of backwards-incompatibility between this standard and subclause 16.14 of IEEE Std 1800-2005. In the 2005 definition, en would have been detected as the inferred enabling condition (a definition that no longer exists in this standard) of a9 and always sampled, so a9 and a10 would have identical behavior." |
|
(0007579) Stuart Sutherland (manager) 2008-10-01 21:19 |
The changes requested in bug notes 7521, 7525, 7544, and 7558 were implemented in draft 7a. |
|
(0007604) Erik_Seligman (developer) 2008-10-07 08:41 |
One more editorial note found by Manisha during review: Page 407 (Sec 16.15.6.1) ------------- // Assume for this example that (posedge clk) will not occur at time 0 always @(posedge clk) begin int i = 10; for (i=0; i<10; i++) begin a8: assert property (foo[const'(i)] && bar[i]) else $error("a8 failed for const i=%d and i=%d", const'(i), i);; ------------ That last line should read: $error("a8 failed for const i=%d and i=%d", const'(i), $sampled(i)); |
|
(0007620) Stuart Sutherland (manager) 2008-10-08 21:08 |
The changes requested in bug note 7604 were implemented in draft 7a. |
|
(0007787) Neil Korpusik (administrator) 2008-12-19 17:59 |
I verified the last change made by the Editor in 1800-2009 draft 8. Changing the status to closed. |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2008-05-27 16:07 | Erik_Seligman | New Issue | |
| 2008-05-27 16:07 | Erik_Seligman | Type | => Enhancement |
| 2008-05-27 16:08 | Erik_Seligman | Assigned To | => Erik_Seligman |
| 2008-05-27 16:08 | Erik_Seligman | Status | new => assigned |
| 2008-05-27 16:09 | Erik_Seligman | Relationship added | related to 0001995 |
| 2008-05-27 16:09 | Erik_Seligman | Relationship added | related to 0001674 |
| 2008-05-27 16:09 | Erik_Seligman | Relationship added | related to 0001900 |
| 2008-05-27 16:10 | Erik_Seligman | Issue Monitored: Erik_Seligman | |
| 2008-05-28 00:20 | shalom | Issue Monitored: shalom | |
| 2008-06-10 18:33 | Erik_Seligman | File Added: concurrent_procedural2_es080610.doc | |
| 2008-06-16 06:18 | Dmitry Korchemny | Category | SV-AC => SV-SC |
| 2008-06-20 09:48 | Erik_Seligman | File Added: concurrent_procedural2_es080619.pdf | |
| 2008-06-20 09:49 | Erik_Seligman | File Added: concurrent_procedural2_es080619.doc | |
| 2008-06-29 11:17 | Erik_Seligman | File Added: concurrent_procedural_es080628.doc | |
| 2008-06-29 11:17 | Erik_Seligman | File Added: concurrent__procedural_es080628.pdf | |
| 2008-07-07 14:32 | Erik_Seligman | File Added: concurrent_procedural_es080707.doc | |
| 2008-07-07 14:33 | Erik_Seligman | File Added: concurrent__procedural_es080707.pdf | |
| 2008-07-09 08:03 | Erik_Seligman | File Deleted: concurrent_procedural2_es080610.doc | |
| 2008-07-09 08:03 | Erik_Seligman | File Deleted: concurrent_procedural2_es080619.pdf | |
| 2008-07-09 08:03 | Erik_Seligman | File Deleted: concurrent_procedural2_es080619.doc | |
| 2008-07-09 08:04 | Erik_Seligman | File Deleted: concurrent_procedural_es080628.doc | |
| 2008-07-09 08:04 | Erik_Seligman | File Deleted: concurrent__procedural_es080628.pdf | |
| 2008-07-09 08:04 | Erik_Seligman | File Added: concurrent_procedural_es080709.doc | |
| 2008-07-09 08:05 | Erik_Seligman | File Added: concurrent_procedural_es080709.pdf | |
| 2008-07-14 09:19 | Erik_Seligman | File Added: concurrent_procedural_es080714b.doc | |
| 2008-07-14 09:19 | Erik_Seligman | File Added: concurrent_procedural_es080714b.pdf | |
| 2008-07-15 16:16 | Erik_Seligman | File Added: concurrent_procedural_es080715b.pdf | |
| 2008-07-15 16:16 | Erik_Seligman | File Added: concurrent_procedural_es080715b.doc | |
| 2008-07-18 10:05 | Erik_Seligman | File Added: concurrent_procedural_es080717b.doc | |
| 2008-07-18 10:06 | Erik_Seligman | File Added: concurrent_procedural_es080717b.pdf | |
| 2008-07-18 10:07 | Erik_Seligman | File Deleted: concurrent_procedural_es080707.doc | |
| 2008-07-18 10:08 | Erik_Seligman | File Deleted: concurrent__procedural_es080707.pdf | |
| 2008-07-21 09:44 | Erik_Seligman | File Added: concurrent_procedural_es080721.doc | |
| 2008-07-21 09:45 | Erik_Seligman | File Added: concurrent_procedural_es080721.pdf | |
| 2008-07-22 07:44 | Erik_Seligman | File Added: concurrent_procedural_es080722.doc | |
| 2008-07-22 07:44 | Erik_Seligman | File Added: concurrent_procedural_es080722.pdf | |
| 2008-07-23 09:31 | Erik_Seligman | File Added: concurrent_procedural_es080723.doc | |
| 2008-07-23 09:31 | Erik_Seligman | File Added: concurrent_procedural_es080723.pdf | |
| 2008-07-23 09:33 | Erik_Seligman | Note Added: 0007255 | |
| 2008-07-23 09:33 | Erik_Seligman | Status | assigned => resolved |
| 2008-07-23 09:33 | Erik_Seligman | Resolution | open => fixed |
| 2008-07-23 09:33 | Erik_Seligman | Fixed in Version | => 1800-2009 |
| 2008-08-01 12:12 | Erik_Seligman | Status | resolved => feedback |
| 2008-08-01 12:12 | Erik_Seligman | Resolution | fixed => reopened |
| 2008-08-01 12:12 | Erik_Seligman | Note Added: 0007275 | |
| 2008-08-01 12:12 | Erik_Seligman | File Added: concurrent_procedural_es080801.pdf | |
| 2008-08-01 12:13 | Erik_Seligman | File Added: concurrent_procedural_es080801.doc | |
| 2008-08-01 15:32 | Erik_Seligman | File Added: concurrent_procedural_es080801b.pdf | |
| 2008-08-01 15:32 | Erik_Seligman | File Added: concurrent_procedural_es080801b.doc | |
| 2008-08-01 18:22 | Neil Korpusik | Note Added: 0007277 | |
| 2008-08-03 13:19 | Erik_Seligman | File Added: concurrent_procedural_es080803.doc | |
| 2008-08-03 13:19 | Erik_Seligman | File Added: concurrent_procedural_es080803.pdf | |
| 2008-08-04 10:19 | Erik_Seligman | File Added: concurrent_procedural_es080804.pdf | |
| 2008-08-04 10:20 | Erik_Seligman | File Added: concurrent_procedural_es080804.doc | |
| 2008-08-05 09:37 | Erik_Seligman | Note Added: 0007298 | |
| 2008-08-05 09:37 | Erik_Seligman | Status | feedback => resolved |
| 2008-08-05 09:37 | Erik_Seligman | Resolution | reopened => fixed |
| 2008-08-05 11:02 | Neil Korpusik | Note Edited: 0007277 | |
| 2008-08-11 09:04 | Erik_Seligman | Status | resolved => feedback |
| 2008-08-11 09:04 | Erik_Seligman | Resolution | fixed => reopened |
| 2008-08-11 09:04 | Erik_Seligman | Note Added: 0007321 | |
| 2008-08-11 09:05 | Erik_Seligman | File Deleted: concurrent_procedural_es080709.doc | |
| 2008-08-11 09:05 | Erik_Seligman | File Deleted: concurrent_procedural_es080709.pdf | |
| 2008-08-11 09:05 | Erik_Seligman | File Deleted: concurrent_procedural_es080714b.doc | |
| 2008-08-11 09:06 | Erik_Seligman | File Deleted: concurrent_procedural_es080714b.pdf | |
| 2008-08-11 09:06 | Erik_Seligman | File Deleted: concurrent_procedural_es080715b.pdf | |
| 2008-08-11 09:06 | Erik_Seligman | File Deleted: concurrent_procedural_es080715b.doc | |
| 2008-08-11 09:10 | Erik_Seligman | File Added: concurrent_procedural_es080811b.pdf | |
| 2008-08-11 09:10 | Erik_Seligman | File Added: concurrent_procedural_es080811b.doc | |
| 2008-08-11 09:18 | Erik_Seligman | File Deleted: concurrent_procedural_es080811b.pdf | |
| 2008-08-11 09:18 | Erik_Seligman | File Deleted: concurrent_procedural_es080811b.doc | |
| 2008-08-11 09:18 | Erik_Seligman | File Added: concurrent_procedural_es080811b.doc | |
| 2008-08-11 09:19 | Erik_Seligman | File Deleted: concurrent_procedural_es080811b.doc | |
| 2008-08-11 09:19 | Erik_Seligman | File Added: concurrent_procedural_es080811b.pdf | |
| 2008-08-11 09:20 | Erik_Seligman | File Added: concurrent_procedural_es080811b.doc | |
| 2008-08-13 15:23 | Erik_Seligman | File Added: concurrent_procedural_es080813.doc | |
| 2008-08-13 15:24 | Erik_Seligman | File Added: concurrent_procedural_es080813.pdf | |
| 2008-08-18 10:06 | Mike Burns | File Added: checkers_part2_080818mb.doc | |
| 2008-08-18 10:07 | Mike Burns | File Added: checkers_part2_080818mb.pdf | |
| 2008-08-18 10:07 | Mike Burns | File Deleted: checkers_part2_080818mb.doc | |
| 2008-08-18 10:07 | Mike Burns | File Deleted: checkers_part2_080818mb.pdf | |
| 2008-08-18 16:56 | Neil Korpusik | Note Added: 0007351 | |
| 2008-08-21 10:35 | Erik_Seligman | Note Added: 0007388 | |
| 2008-08-21 10:35 | Erik_Seligman | Status | feedback => resolved |
| 2008-08-21 10:35 | Erik_Seligman | Resolution | reopened => fixed |
| 2008-08-23 09:27 | Neil Korpusik | Note Added: 0007390 | |
| 2008-08-28 09:22 | Neil Korpusik | Note Added: 0007401 | |
| 2008-08-28 09:22 | Neil Korpusik | Status | resolved => approved |
| 2008-09-11 05:43 | Stuart Sutherland | Status | approved => completed |
| 2008-09-11 05:43 | Stuart Sutherland | Fixed in Version | 1800-2009 => P1800-2009/D7 |
| 2008-09-11 05:43 | Stuart Sutherland | Note Added: 0007499 | |
| 2008-09-15 09:22 | Erik_Seligman | Note Added: 0007521 | |
| 2008-09-15 09:22 | Erik_Seligman | Status | completed => editor |
| 2008-09-16 10:13 | gordonv | Note Added: 0007525 | |
| 2008-09-22 09:49 | Erik_Seligman | Note Added: 0007544 | |
| 2008-09-26 03:04 | shalom | Relationship added | related to 0002483 |
| 2008-09-30 13:17 | Lisa Piper | Note Added: 0007558 | |
| 2008-10-01 21:19 | Stuart Sutherland | Status | editor => completed |
| 2008-10-01 21:19 | Stuart Sutherland | Note Added: 0007579 | |
| 2008-10-07 08:41 | Erik_Seligman | Note Added: 0007604 | |
| 2008-10-07 08:41 | Erik_Seligman | Status | completed => editor |
| 2008-10-08 21:08 | Stuart Sutherland | Status | editor => completed |
| 2008-10-08 21:08 | Stuart Sutherland | Note Added: 0007620 | |
| 2008-11-05 19:22 | shalom | Relationship added | related to 0002516 |
| 2008-12-19 17:59 | Neil Korpusik | Status | completed => closed |
| 2008-12-19 17:59 | Neil Korpusik | Note Added: 0007787 | |
| 2009-01-08 07:29 | Neil Korpusik | Relationship replaced | has duplicate 0001995 |
| Mantis 1.1.7[^] Copyright © 2000 - 2008 Mantis Group |  |
