| 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 | |||
| 0001900 | [SystemVerilog P1800] SV-SC | feature | 2007-06-25 09:52 | 2008-12-19 17:45 | |||
| Reporter | Erik_Seligman | View Status | public | ||||
| Assigned To | Dmitry Korchemny | ||||||
| Priority | high | Resolution | fixed | ||||
| Status | closed | Product Version | |||||
| Summary | 0001900: Add new 'checker' construct to SVA | ||||||
| Description | See the attached proposal. We are suggesting a new construct which will enable better support for next-generation OVL-like libraries and for encapsulation of formal modelling. | ||||||
| Additional Information | |||||||
| Tags | No tags attached. | ||||||
| Type | Enhancement | ||||||
| Attached Files |
|
||||||
|
|
|||||||
Relationships |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Notes |
|
|
Erik_Seligman (developer) 2007-08-21 07:06 |
The version I posted yesterday (8/20) is a working draft-- I'm still revising it with Dmitry, so many changes are expected. |
|
Dmitry Korchemny (manager) 2007-11-26 09:45 |
Made some minor fixes according to Erik's notes. |
|
Dmitry Korchemny (manager) 2007-12-10 07:21 |
Renamed "free variables" to "checker variables" (checkvar). Now checker variables must be deterministic unless 'free' qualifier is explicitly specified. |
|
John Havlicek (manager) 2008-01-27 08:36 |
2008-01-15: Passed by e-mail vote, 7y/0n/3a. There was a friendly amendment. |
|
John Havlicek (manager) 2008-01-27 08:38 |
2008-01-21: Revision to address friendly amendments passed by e-mail vote, 6y/0n/4a. There were no additional friendly amendments. |
|
Dmitry Korchemny (manager) 2008-01-29 03:46 |
Addressing champions' review (Shalom's comments), and comments from TT and YF. |
|
Dmitry Korchemny (manager) 2008-01-29 06:05 |
Rolling back to the original version in order not to change the version during the champions' ballot. Will address all the champions' feedback at once when the ballot is over. |
|
Neil Korpusik (administrator) 2008-02-08 19:08 |
The proposal failed in the Champions email vote which ended on Feb 4th, 2008. Failed with 2 no-votes - Dave - This proposal needs to be addressed when it can have the full attention of all the committees as effects every part of the language. Otherwise, I feel that this enhancement goes beyond the level of enhancements authorized by the P1800 PAR in embedding a new language with SV. The number of keywords and statements being introduced can not be thoroughly reviewed with the resources we have for the current par. A suggestion would be to call a join meeting to have the SV-AC present this proposal to members of all the other committies as part of a design review. - Shalom - Sent a lot of feedback to the sv-ac (in 5 parts). - John - Friendly amendments: Rationale for Abstain: I collected too many friendly amendments below to justify a clear "Yes" vote, and I'm still going carefully though the last 10 pages of the proposal. Friendly Amendments: - 16.18.1, p. 8. I'm not sure that the following sentence is precise enough to interpret what "remains valid" means: If the fact that the abstract model is indeed an abstraction of a concrete model can be formally proven then the reasoning about the abstract model behavior remains valid for the behavior of the concrete model. Presumably, there is a correspondence between the behaviors. In any case, I don't think this statement is needed in the LRM. - 16.18.2, p. 11. In If a formal argument is written in the checker body, its corresponding actual argument shall be a checker variable or a formal argument in another checker. I recommend changing "formal argument is written" to "formal argument is assigned a value". This is for consistency with the other sentences in this paragraph. - 16.18.4, p. 14. There is a type mismatch in the example with check_in_context. The formal argument enable is of type logic, but the instance my_check1 binds to it the sequence expression "en1 ##1 en2". One solution is to change the actual to something like "en1 || en2" and also change the parenthetical clause: note also that a sequence has been passed to the checker as its enabling condition Alternatively, the type of the formal argument should be changed. - 16.18.5, p. 16. The following sentence As regular variables, checker variables can be packed or unpacked aggregates of other types (see 6.5). should be reworded for clarity. The phrase "as regular variables" could be omitted entirely or changed to something like "as in the case of regular variables". - Editorial: 16.18.5, p. 16. Change "show" to "shows" in "The following example show". - 16.18.6, pp. 16-17. The intuitive descriptions of the assumptions imposed on the free checkvar bit flag seem reasonable for a formal tool in which $global_clock ticks at every point in time. In simulation, however, $global_clock may not be at the granularity of a timestep and a simulator may apply chaotic values for flag in timesteps that are not ticks of $global_clock. In this situation, the intuitive descriptions do not seem accurate. I recommend either 1. Stating that it is assumed that $global_clock ticks at every timestep, or 2. Qualifying the intuitive descriptions in a way that makes it clear that they apply only in the timesteps in which $global_clock ticks. - 16.18.6, p. 18. If a simulator cannot assign a right value needs to be reworded to clarify what "assign a right value" is intended to mean. - 16.18.6, p. 18. which in turn implies that the corresponding legality of data transfer through that transaction is being checked. The legality might not be checked in simulation because the simlator might choose the wrong value for mem_data. I think this sentence needs to be worded in a way that does not suggest that checking of legality is ensured in simulation. - Editorial: p. 19. Change "as opposite to" to "as opposed to". - 16.18.6.1, p. 19. In Example 1, the constant "3'b3" should be something like "3'd3" or "3'h3". Similarly with "3'b5". - 16.18.6.1, p. 20. I would change "the clock of the sequence" to "the ending clock of the sequence" in In nonblocking assignments the matched method provides synchronization between the clock of the sequence I would also change "when the sequence clock" to "when the ending clock of the sequence" in the sentence that follows (2 places). In the examples that follow, the second "endsequence : s1" should be "endsequence : s2". Also, we don't really have enough information to conclude the following: On the contrary, the value of u at time 90 will be 0 since there is no match of s2 at time 90. This statement assumes that there is not another match of s2 ending at 90. - 16.18.6.1, p. 20. I recommend deleting "Thus," from Thus, an unpacked structure or array can have one element assigned procedurally and another element assigned continuously. This conclusion does not follow from the preceding. Also, "can" should probably be "may". - 16.18.6.1, p. 21. I'm not sure how the SAR is interpreted when the check bit to be assigned may be determined dynamically. In Example 4, the discussion says that there is a SAR violation for counter[0]. Is this just because i may take the value 0? Is the following legal free checkvar bit [5:0] counter; free checkvar bit [1:0] i; assign counter [5:4] = foo; always_check @clk counter[i] <= !counter[i]; ? - 16.18.6.4, p. 26. The shifting of the NBA when future value functions appear in the RHS may produce counterintuitive results in simulation if the $global_clock is not the fastest. |
|
Dmitry Korchemny (manager) 2008-02-10 07:37 |
Reopened to address the champions' feedback. |
|
Dmitry Korchemny (manager) 2008-02-20 11:56 |
Added a clock wave to fig.16-17 as suggested by SB. |
|
John Havlicek (manager) 2008-02-26 10:30 |
2008-02-26: Voice vote to approve checkers_080225_part1_dk.pdf and checker_080225_part2_dk.pdf, 9y/0n/0a. |
|
John Havlicek (manager) 2008-02-28 08:39 |
2008-02-28: Voice vote 7y/0n/0a to approve the 2008-02-27 .pdf version, parts 1 and 2. |
|
Dmitry Korchemny (manager) 2008-03-25 14:37 |
Reopened to update dependcies as requested by Champions 2008-03-20. |
|
Neil Korpusik (administrator) 2008-04-23 11:05 |
Moving to the sv-sc. |
|
Erik_Seligman (developer) 2008-07-23 09:25 |
Passed voice vote at SV-SC meeting, 2008-07-22, conditional on some specific minor edits (implemented in version posted by Erik Seligman on 2008-07-23). 9y/0n/3a Neil and Francoise abstained due to not enough time to review. Steven Sharp abstained because he believes it is under-researched and too many changes have been made too quickly, though he has not actually spotted any specific problems. |
|
Mike Burns (developer) 2008-08-07 16:26 |
Addressing champions feedback |
|
Neil Korpusik (administrator) 2008-08-18 16:59 |
Part 2 of the proposal was sent back to the sv-sc by the Champions in the August 7th, 2008 conference call. There have been several updates to the proposal since this Champion's meeting took place. This bug note is here to document the list of issues that were flagged in the Champion's meeting. 2.3 1900 SV-SC Add new 'checker' construct to SVA List of Changes required: 1. Part 2, p. 6. In the example, is v1 static? If so, then I think that the declaration assignment is performed only once, so the behavior of check_loop is not described correctly. This could be fixed by making v1 automatic or by changing logic [7:0] v1=0; to logic [7:0] v1; v1 = 0; Also see a mantis 1556, which is related to this situation. 2. Part 2, p. 13. It is stated that the assume set of F1 excludes F1.B1.u2 because the only formal argument of the child checker bar is bound to actual r that is an inactive free variable. Is it true that F1.B1.u2 is in the assume set of F1.B1? I think that the rules say that it is. We left this question for the committee to answer. John wants to make sure his understanding is correct. 3. Part 2, p. 14. Miscounting of cycles for the example at the top of the page x |=> ##5 1'b0 // |=> includes a one clock cycle delay. From: "... it would inevitably fail five clock cycles later." To: "... it would inevitably fail six clock cycles later." 4. Part 2, p. 14. The exception to Preponed sampling for constants and automatics is too tight. Local variables are excluded, as are the active free checker variables. In the last paragraph of 17.6.3 "Concurrent assertions have invariant scheduling semantics - whether present in checker code or design code. These assertions always sample the values available while processing the Preponed region, except for constants or automatics as described in Reference to 2398, <add the following text here> and they are always evaluated when processing the Observed region." "local variables, and free checker variables" 5. Page 2, next to the last dash list, mentions automatic variables. Can a checker contain a loop, in particular, a SystemVerilog style loop, where the loop index variable has automatic lifetime? It would be confusing if can't use the declaration in the loop. This point should be made more clear. 6. page 4, bottom, "A checker may be instantiated in one of the following, where a concurrent assertion may appear" a. From: "A checker may be instantiated in one of the following..." To: "A checker may be instantiated wherever a concurrent assertion may appear (see 16.15)." b. The cross reference also seems to be wrong (16.14) should be 16.15. c. Don't need the list on p4. d. Need to add generate block to the list in 16.15? 7. Part 1 adds an item to the list in 16.15. A generate block is not in part 1. (Missing?) This may cause a chain reaction of changes (is it in 1728?) 1728 had the effect of propagating it to many places. The two should be consistent. 8. Global issue throughout the proposal (ref: mantis 2398) 0002398 touches a bunch of sections. The sv-sc should figure out the right cross references as much as possible. Check all of the cross-references (taking 2398 into account). 9. Page 5, bottom, last sentence, "Procedural assertion statements" "Procedural assertion statements, assertion statements within a procedural block of a checker, shall be treated just like other procedural assertion statements as described in" This is not worded well. Is the part after the comma suppose to be a definition of a procedural assertion statement? 0002398 makes a distinction between static and concurrent. Can there be an immediate assertion in a checker? 10. Page 6, example, header of module m, "int [20:0] foo" is illegal. bit [20:0] might be what was intended. There was also a problem in 2398. (const apostrophe) const ` has the tick going the wrong way on page 6 of part2. 11. Shalom - p6, "foo[const`(v1)]" is selecting a single bit. a. Was the intent to use 8 bits? Maybe foo should be an array of bytes b. Change names foo, bar to something more meaningful. 12. 17.5, p8, "event control statement", an event control is not a statement 13. page 8, "monitored only on the first clock tick" was deleted by 2398. Reconcile 1900 part2 with the changes in 2398 14. Page 9, near top "A free variable may assume any value at every point in time. Formal analysis tools shall take into account all possible values of the free checker variables imposed by the assumptions and assignments (see 17.6.1). Simulators shall assign random values to the free variables as explained in 17.6.2" Not sure what this means, "every point in time". At every time step, can have a different value? Was the intent meant to be - every tick of the global clock? 15. Page 9, after example, 2nd bullet, "If there is a reset, it becomes low at the next tick of the clock." It wasn't quite clear what was being stated |
|
Neil Korpusik (administrator) 2008-08-18 17:25 |
Results of the Champion's email vote which ran for 6 days, ending on Wednesday, August 13th (7pm PST). 3. 1900 Approve part2, pages 10-16 - motion failed (2y,3n,0a) No : Dave -- see details below Yes : Brad -- see details below No : Stu -- see details below Yes : John No : Shalom -- see details below Note: 0001900, part2 was only partially reviewed in the Champion's conference call of August 7th. The purpose of this email vote is to get out on the table any remaining issues with the remainder of the proposal. Detailed feedback: ------------------ Dave: 3. 1900 Approve part2, pages 10-16 Yes ___ No _X__ [DR] I echo Stu's comments. Although the SV-SystemC has made great progress (and none of that effort will go to waste) I am not comfortable going to ballot in its current state. Stu: 3. 1900 Approve part2, pages 10-16 Yes ___ No _X_ Abstain ___ I vote No because there has been a lot of very recent e-mail traffic with questions and issues, which indicates that the proposal needs further clarification and review. To the SC committee's credit, they have been very quick to fine tune the proposal in response to some of the e-mail traffic, but I am concerned that these revisions are bypassing the review and approval process of the full SC committee. Brad: I vote 'Yes' on all 3, with the comments that --- 1900-1 --- The following formulation is strange "A checker may be instantiated wherever a concurrent assertion may appear (see 16.15). It shall be illegal to instantiate checkers in fork...join, fork...join_any, or fork...join_none blocks." I assume the first sentence is intended to imply that a checker may not appear in places where concurrent assertions may not appear. But then wouldn't the second sentence be redundant? Shouldn't it be "In particular, it is illegal to instantiate ..."? It's also strange that this second sentence begins a new paragraph. --- 1900-2 --- Because these are redundant "modules, interfaces and programs shall not be either declared or instantiated inside checkers" "Modules, interfaces and programs shall not be instantiated inside checkers." In the first sentence it would be better to delete "either" and "or instantiated". --- 1900-3 --- A checker can be declared within a checker, yet checker declarations are not listed after "A checker body may contain the following elements ..." --- 1900-4 --- Why is there no mention of packages in this sentence? "Checkers may be declared inside modules, programs, interfaces, and other checkers, but modules, interfaces and programs shall not be either declared or instantiated inside checkers." Shalom: > > 3. 1900 Approve part2, pages 10-16 Yes ___ No _x__ > > Abstain ___ I have described my reservations about the description of the assume set in separate mails. Not all my doubts have been settled yet. I also have some additional issues. P. 9: "Simulators will assign random values to the variable flag as explained in 17.6.2." Change "will" to "shall", "flag" to Code font. P. 10: "Simulators assign a random constant value to a constant free variable as explained in 17.6.2." Change "assign" to "shall assign". P. 10: "Memorizing data". Change to something else, such as "Data integrity checking". P. 10: "// If start_ev is asserted then the value of in_data has to be // equal to the value of out_data at the next assertion of end_ev" Really it is checking the reverse, that out_data at end_ev will be equal to in_data at start_ev. P. 11: "However at a given time step all occurrences of a non-constant checker variable have the same value, e.g., the assertion rand bit a; assert property (@clk a == a); // clk defined elsewhere is a tautology: though at different time steps a may assume any value: 0 or 1 - this value is the same for both occurrences of a." I found this extremely confusing. The apparent meaning was so obvious that I looked for a different, less obvious meaning. I was also not sure what was meant my "occurrence". I think this should just be deleted. The way free checker variables get values is described in detail later on anyway. P. 11: "The right-hand side of a checker variable assignment may contain sequence method triggered (see 16.14.6)." Change "sequence method" to "the sequence method". P. 13: "All other variables (such as non-free checker variables and checker formals) are always treated as inactive, as are all past values of free checker variables." "Past values" are just that, past. How could they possibly be treated as active? What is the point of this part of the sentence? P. 13: "Note that since assumptions are evaluated as simulation assertions as well as being used for randomization, each assume statement potentially contributes many assertions to the pending procedural assertion queue, even though it only contributes once to an assume set." This is not clear. What is being referred to? What is an example? Does it even need to be stated? P. 13: "bar B1(clk, q+r, r);" "clk" should be "fclk"? P. 14, et al.: "timestep" should be "time step". P. 14: "When an implementation is about to begin the Observed region, it must solve for all the active free variables." Change "must" to "shall". P. 14: "Note that checker procedures and properties execute in the Reactive and Observed regions (see 17.7), and so have the new values available." I think the reference is wrong. It should be 17.6.3 ? P. 15: "Expressions at the right hand side of checker variable assignments are allowed to include function calls with the same restrictions that are imposed to function calls in concurrent assertions (see 16.6): - Functions that appear in expressions cannot contain output or ref arguments (const ref is allowed). - Functions should be automatic (or preserve no state information) and have no side effects." Change "to function calls" to "on function calls". Change "cannot contain" to "shall not contain". Change "should be automatic" to "shall be automatic". (Yes, I know that text is copied from 16.6. The changes are needed there also.) |
|
Erik_Seligman (developer) 2008-08-21 10:36 |
Final edits approved in SV-SC voice vote, 8/19/2008. |
|
Neil Korpusik (administrator) 2008-08-23 09:32 |
The proposal was approved by the Champions in the August 21st, 2008 conference call with one abstain. Move: Brad - approve the proposal for 0001900 Second: John Abstain: Dave - Fundamentally opposed to adding this to the current PAR. - Can't do an adequate technical job for something that has not been implemented. Passed with one abstain |
|
Neil Korpusik (administrator) 2008-08-28 09:26 |
The proposal was approved by the Working Group in the continuation of the August 14, 2008 conference call, which was held on August 28, 2008. There was one Opposed. Dennis (Mentor) - let stand Dave Rich's comment from the Champions vote "Dave is fundamentally opposed to adding this to the current PAR. We can't do an adequate technical job for something that has not been implemented." |
|
Stuart Sutherland (manager) 2008-09-11 00:44 |
The change proposal was implemented in draft 7. |
|
Erik_Seligman (developer) 2008-09-15 12:31 |
I have reviewed sections 17.1-17.4 of Part 2 in Draft 7. I noticed one minor issue: in 17.3, p. 428, 2nd bullet point near the bottom, "If an actual argument contains any subexpression that is a const cast..." I think the word 'const' should be in courier, as it was in the proposal doc. |
|
Lisa Piper (developer) 2008-09-17 07:33 |
I reviewed my sections 17.5 - end and have the following comments: In 17.6.1, there is a link to F.3.4.6 that should be to “F.3.4.9 Checker variable assignment” In 17.7.2, there is a reference to “non-const” (2nd word of 3rd paragraph). Const should be bold courier the way it is in the next paragraph. The same applies to the word const in “is a const cast” in the 6th paragraph of that same section. In 17.7.2, the paragraph that starts “The assume set of F1 consists of …” should be split into two paragraphs starting at “When a solution attempt is made …” In F.3.4.9, there exists two “=” signs that should be “?” as shown below — rand t u = e ? initial assume property (@1 u === e) — always @c u <= e ? always assume property (@1 $future_gclk(u) === c ? e : u) |
|
Tom Thatcher (developer) 2008-09-22 10:24 |
I reviewed Part 1 of the proposal, and found two minor issues In 3.11 Overview of Hierarchy, The sentence reads: "When a module contains an instance of another module, interface or program or checker, . . ." It should read: "When a module contains an instance of another module, interface, program, or checker, . . ." In A.6.10, the construct "deferred_immediate_assertion_item" was added twice, once as the second item, and once again later in that subclause. |
|
Dmitry Korchemny (manager) 2008-09-24 06:54 |
• 3.9 Packages The following change was not implemented: "Identifiers declared within a module, interface, or program are local to that scope, and do not affect or conflict with declarations in other building blocks." --> "Identifiers declared within a module, interface, program, or checker are local to that scope, and do not affect or conflict with declarations in other building blocks." • 3.11 Overview of hierarchy The second sentence "When a module contains an instance of another module …" has a wrong markup: the comma after "interface" should be inserted, and "or" before "program" should be deleted. The Draft7 the markup reads the opposite. • A.9.3 The layout of checker_identifier should be the same as for other identifiers in this subclause |
|
Dmitry Korchemny (manager) 2008-09-24 23:47 |
• 3.9 Packages The following change was not implemented: "Identifiers declared within a module, interface, or program are local to that scope, and do not affect or conflict with declarations in other building blocks." --> "Identifiers declared within a module, interface, program, or checker are local to that scope, and do not affect or conflict with declarations in other building blocks." • 3.11 Overview of hierarchy The second sentence "When a module contains an instance of another module …" has a wrong markup: the comma after "interface" should be inserted, and "or" before "program" should be deleted. The Draft7 the markup reads the opposite. • A.9.3 The layout of checker_identifier should be the same as for other identifiers in this subclause |
|
Eduard_Cerny (developer) 2008-09-25 10:52 |
In A.6.10 the definition of deferred_immediate_assertion_item ::= [ block_identifier : ]deferred_immediate_assertion_statement is duplicated. The 2nd occurrence on page 1118 could be deleted. |
|
Mike Burns (developer) 2008-09-25 14:43 |
The cross-reference in 17.7, p.435 "The latter example may be rewritten for formal verification using local variables instead of constant free variables (see 16.9.." refers to the wrong section both in the proposal and in Draft 7; it should be 16.10 - the section on local variables. 17.7.1 - editor's question - is the ref correct? No - it should be F.3.4.9 rather than F.3.4.6. 17.7.2 first example "mymod", u3 and u4 are over-indented; they should be indented to the level of the "rand bit q, r;" declaration above. 17.7.2 paragraph 7: "neither of those assume statements involve formals" - "assume" should be bold courier font. 17.9: "generate if (coverage_level != ovl_cover_none) begin : cover_b" - the "ovl_cover_none" should be "cover_none" (the proposal has the same error). 17.9: The two cover properties at the end of the example should have the keywords "cover" and "property" in bold font. |
|
Stuart Sutherland (manager) 2008-10-01 19:20 |
The changes requested in bug notes 7522, 7528, 7545, 7550, 7551, 7552 and 7554 were implemented in draft 7a. |
|
Erik_Seligman (developer) 2008-10-08 08:06 |
Some notes from Mirek. I think these can be fixed editorially at this stage. --------------- 17.4 Context inference, page 425, there is: "Context value functions (see 16.15.6) [...]" it shall be: "16.15.7" (which is: Inferred value functions) This is an issue in draft7 edition, for draft6 the 16.15.6 was correct, in draft7 it is 16.15.7, so the reference in shall be updated while implementing proposal text into draft7. ---------------- 17.3 Checker instantiation, page 422: A.4.1.4 Checker instantiation, page 1078: there is: ordered_checker_port_connection ::= { attribute_instance } [ property_expr ] named_checker_port_connection ::= { attribute_instance } . port_identifier [ ( [property_expr] ) ] | { attribute_instance } .* it shall be "property_actual_arg" instead of "property_expr" in both: ordered_checker_port_connection and named_checker_port_connection productions, otherwise the code as in example: 17.3.1. Behavior of instantiated checkers, page 423 ... c1 check_outside(posedge clk, in1, in2); ... would be illegal. ----------------------------- |
|
Erik_Seligman (developer) 2008-10-08 08:23 |
More notes from my cross-review of 16.8-16.10: - 16.8, bulleted list at start of section: since we are enumerating places where a sequence can be defined, we need to include -- A checker - 16.8.1, in text just before "delay_arg_example", the keyword "shortint" is separated across two lines with a dash. Is it legal to split a keyword like this, or do we need to keep it one one line? - 16.10: This discussion of local variables in sequences and properties occurs before we have introduced properties, which are coming in section 16.13, and thus might be hard to follow for someone not already familiar with the standard. I think 16.10 should be moved after 16.13, in other words renumbering the sections as: 16.10 -> 16.13 16.11->16.10 16.12->16.11 16.13->16.12. If this is too much change at this stage, alternatively we should include a reference to 16.13 when properties are first mentioned, in the first sentence of 16.10. |
|
Stuart Sutherland (manager) 2008-10-08 20:23 |
The changes requested in bug notes 7605 ande 7606 were implemented in draft 7a. |
|
Mike Burns (developer) 2008-10-13 11:35 |
My previous state change was a mistake - I'm changing it back to completed. |
|
Dmitry Korchemny (manager) 2008-10-23 02:13 |
16.13 Declaring properties: bulleted list at start of subclause should include -- A checker |
|
Dmitry Korchemny (manager) 2008-10-23 02:39 |
16.13 ----- . The use of "a checker" in the second sentence of the section clashes with the new checker construct and should be changed to "an obligation". (John Havlicek) |
|
Dmitry Korchemny (manager) 2008-10-23 02:42 |
16.13 ----- . The use of "a checker" in the second sentence of the section clashes with the new checker construct and should be changed to "an obligation". (John Havlicek) |
|
Dmitry Korchemny (manager) 2008-10-23 04:22 |
16.13.17 -------- . First paragraph, change Recursion provides a flexible framework for coding properties to serve as ongoing assumptions, checkers, or coverage monitors. to Recursion provides a flexible framework for coding properties to serve as ongoing assumptions, obligations, or coverage monitors. Rationale: With the checker construct, the word "checker" should be avoided in this context. (John Havlicek) |
|
Dmitry Korchemny (manager) 2008-11-04 22:59 edited on: 2008-11-05 02:39 |
* The bullet color of the item - endchecker in 9.3.4 Block names is blue, but should be black. * Same in 16.8 Declaring sequences - A checker. |
|
Stuart Sutherland (manager) 2008-12-02 21:34 |
The changes requested in bug note 7652, 7653, 7654, 7644 and 7697 were implemented in draft 8. |
|
Neil Korpusik (administrator) 2008-12-19 17:44 |
I verified the set of changes made by the Editor for 1800-2009 draft 8. Changing the status to closed. |
|
Neil Korpusik (administrator) 2008-12-19 17:45 |
I verified the set of changes made by the Editor for 1800-2009 draft 8. Changing the status to closed. |
| Mantis 1.1.7[^] Copyright © 2000 - 2008 Mantis Group |