Fixes needed to current proposals

• Proposals not in draft 5 (but slated for draft 6) were reviewed by SV-SC
• Changes that will be affected by our proposed additions to concurrent asserts, checkers, and 'let' were identified.
• Current plan is that amendments will be included in new proposals. Alternative: publish new versions of old proposals.
• Proposals can be found on Mantis: http://www.verilog.org/mantis/view.php?id=nnnn

TBA

• 1901, 1800 (Dave)

Proposals identfied as not needing changes

• 2171 (Ed), 2005, 1932 (Erik), 1758 (Jin), 1682, 1683 (Dmitry), 1641 (Mike), 2033 (Mark), 2336, 2250 (Abi), 1731, 1729 (Manisha), 2090, 2069 (Tom), 2335, 2188 (Steve), 1698, 1687, 1686 (Gord), 1757 (Neil)

Changes needed

• 2175: D4 implementation feedback (Ed): Only partially usable, essentially the changes on page 1 only. The rest in clause 16.14.6 should be changed or scrapped altogether based on the new proposal (2398) for inference of enabling condition (if such a thing still exists) and the way assertions are triggered in procedural code.
• 1648: Default Disable (Lisa): There is one example that may need clarification. I am thinking it would be best to simply reference the new section (of 2398) that talks about inferred enabling conditions. "In 16.15 Disable iff resolution, change:..." See full change at http://www.eda-stds.org/sv-sc/hm/0168.html.
• 2100: Synchronous Aborts (Lisa): Mantis 2100 on synchronous aborts has multiple examples that reference @(clk). It is not clear to me whether this needs to change – I missed that discussion. Also, is it @edge clk or @(edge clk)?
• 2091: where concurrent discussions can be placed (Lisa): It states that current values are used for local vars and loop indices and for everything else the sampled value is used. I think this should also state that any inferred enabling condition would use the current value (to sync with 2398). See full change at http://www.eda-stds.org/sv-sc/hm/0168.html.
• 1769: Elaboration-time user error messages (Jin): usage of elaboration-time user error messages needs to be defined in the checker context (for 1900).
• 1681: Global Clocking (Mike): We need to account for "edge clk" here.
• 1601: Untyped Keyword (Mike): Unaffected, but very close. It should be checked, after composing with other proposals (1549?), that the resulting draft accurately reflects committee's intent w.r.t. semantics of passing expression actuals to untyped formals of sequences and properties.
• 1987: Assertion Statements (Mark): I assume that everyone agrees that a 'checker' is not an assertion statement (clarify in 1900). This proposal does make wording changes to 16.14.6 on inferred enables which will be completely replaced. These changes are from "verification statement" to "assertion statement". (in light of 2398)
• Annex F from Draft 5: (John): The overview should say that Annex F does not define the semantics of arming an attempt of a concurrent assertion in procedural code (2398). Once such an attempt is committed, the semantics of of the underlying property evaluation is defined by Annex F. Item F.2.c.4 of the overview should be removed. References to inferred enabling condition need to be removed from the overview. F.4.3.1. Inferred enabling conditions need to be removed.
• 1667: Local variable arguments. (John).
  • I think that the statement "The self-determined result type of the actual argument shall be cast compatible (see 6.22.4) with the type of the local variable formal argument." should be changed. It implies that the actual argument is treated in a self-determined context, whereas a declaration assignment to a local variable ought to treat the RHS in an assignment context. This should be reviewed with a type expert.
  • When binding an actual to an inout local variable, I think that cast compatibility in both directions (actual to formal and formal to actual) is required. I don't know if cast compatibility is an equivalence relation. For an output local variable, I think that only cast compatibility from formal to actual is required. This should be reviewed with a type expert.
• 2246: vpiAssertionKill (Abi): vpi_control() usages that act to discard assertion attempts-- Need to clarify in relation to 2398.
• 1599: VPI for 805 (Abi): various assertion/coverage interaction changes from 2398.
• 2150: Automatics in action blocks (Manisha): this proposal will change based on how we will treat automatic variables in assertions. If there is going to be any implicit rule about treating automatics as consts for assertions then probably same rule can be applied to action blocks. Currently it disallows automatics in action blocks but treats loop index variable in a special way.
• 2168: Formal semantics for edge-sensitive clocks (John): A definition for "edge b" should be added in the changes for F.2.1.
• 1668: Local variable initializers (John): First change to 16.9, description of using Preponed values for non-local variables appearing in initialization expressions should provide for the mechanism of capturing values to be treated as constant but that need not be Preponed values.
• 1549: Missing argument types (John): Many changes related to self-determined types: see http://www.eda-stds.org/sv-sc/hm/0232.html.
• 1737: (Enabling conditions fix). Discusses concurrent assertions in procedural code and could very well need to be updated.

-- ErikSeligman - 28 May 2008