[sv-ac] Champions feedback from Shalom

From: John Havlicek <john.havlicek_at_.....>
Date: Tue Feb 05 2008 - 06:20:50 PST
Hi Folks:

Below is the ballot from Shalom Bresticker in the most recent
Champions email vote.

This is not the official feedback from Champions, but it is
the vote that Shalom sent together with comments and can be
viewed on the Champions reflector.

J.H.

----------------------------------------------------------------------------

Unmarked items are abstains due to lack of time and/or expertise.

Shalom


List of Mantis items for a Champion's email vote:
-------------------------------------------------
1.  2227    Yes _x_ No ___ Abstain ___ SV-EC  Incorrect comparison of
$random and $urandom
2.  2181    Yes ___ No ___ Abstain ___ SV-EC  Ambiguity in implicit
declaration of production variables in randsequence
3 . 1447    Yes ___ No _x_ Abstain ___ SV-EC  Contradictory stmts about
unsized array dimensions (5.1 vs. 5.7 and 5.8)
I agree with Dave's objection, but I did not review the rest of the
proposal.

4 . 0958    Yes _x_ No ___ Abstain ___ SV-EC  dynamic array size method
unclear when empty
5 . 1858    Yes ___ No ___ Abstain ___ SV-EC  Name binding in inline
constraints
6 . 0520    Yes _x_ No ___ Abstain ___ SV-EC  examples of queues
assignments are not legal array assignments
7 . 2003    Yes _x_ No ___ Abstain ___ SV-EC  Old statement on foreach
for wildcard indexed associative arrays
8.  2221    Yes _x_ No ___ Abstain ___ SV-BC  "unpacked array reference"
is ambiguous
9.  2193    Yes _x_ No ___ Abstain ___ SV-CC  Need to clarify vpiValid
flag
10. 2190    Yes _x_ No ___ Abstain ___ SV-CC  Standard does not say what
should happen when putting value with delay to a dynamic object
11. 2086    Yes _x_ No ___ Abstain ___ SV-CC  Deprecated vpiArray still
used with vpi_register_cb() description
12. 2063    Yes _x_ No ___ Abstain ___ SV-CC  Three minor typos in
sections 36.15, 36.21 and 36.25
13. 2016    Yes ___ No ___ Abstain ___ SV-CC  vpiClassType should apply
to class typespec rather than to class defn
14. 2009    Yes ___ No ___ Abstain ___ SV-CC  HDL example shown in
detail 3 section 36.14 (Reference objects) has errors.
15. 1995    Yes _x_ No ___ Abstain ___ SV-AC  Allow concurrent
assertions and checkers in for loops
Note to the editor: In "For loop control variable value 1, the assertion
will pass, and the pass action block will be generated," change the last
word to "executed".
Dave wrote, "This proposal is essentially creating a generate block
within a procedural context." That was the original intention, but the
proposal was reworked to change that after Gord objected. The proposal
emphasizes that there is only one assertion. See
http://eda.org/sv-ac/hm/5893.html for more info.

16. 1952    Yes ___ No ___ Abstain ___ SV-CC  "Null argument" to mean
"omitted argument" may be confusing
17. 1846    Yes ___ No _x_ Abstain ___ SV-BC  D3 21.13: add 1800-2008 to
`begin_keywords
Superceded by 1826
18. 1826    Yes _x_ No ___ Abstain ___ SV-BC  JEITA: Annex B Add keyword
list by LRM version
19. 1741    Yes ___ No ___ Abstain ___ SV-CC  1800-2005 Section 27.50
Issues with foreach diagram
20. 1729    Yes ___ No ___ Abstain ___ SV-AC  Introduce immediate assume
and cover statements
21. 1728    Yes _x_ No ___ Abstain ___ SV-AC  Introduce "let"statement
Re Dave's objection, "let" was originally planned to be general, but
SV-AC was explicitly requested to limit it to assertions, so that is
what they did. Even Gord said that the final version meets all his
concerns.

22. 1711    Yes _x_ No ___ Abstain ___ SV-BC  Rules for unique case
evaluation
23. 1668    Yes ___ No ___ Abstain ___ SV-AC  Local variable
initializers.
24. 1667    Yes ___ No ___ Abstain ___ SV-AC  Local variable arguments
for sequences and properties.
25. 1549    Yes _x_ No ___ Abstain ___ SV-AC  add missing formal
argument types
26. 1456    Yes ___ No ___ Abstain ___ SV-CC  Clarify, circumscribe
restrictions on use of DPI context utilities
27. 0748    Yes ___ No ___ Abstain ___ SV-CC  vpiParent of var select
can only be array var
28. 1900    Yes ___ No _x_ Abstain ___ SV-AC  Add new 'checker'
construct to SVA

I sent my comments to SV-AC. Here are the most important ones:

In 16.3.6, "The value of method triggered evaluates to true if the given
sequence has reached its end point at that particular point in time and
false otherwise. The triggered status of the sequence is set in the
Observed region and persists through the remainder of the time step.
This method shall only be used in wait statements or boolean expressions
(see 9.4.4) outside of sequence context".
I know that this did not change in this proposal (except for one word),
but since the proposal is already changing the paragraph, I think the
cross-reference to 9.4.4 should be 9.4.5, and "sequence context" should
be "a sequence context" or "sequence contexts".

"The checkers may contain concurrent assertions, checker variable
declarations and assignments, structural procedures," should be
"structured procedures".

16.18.1 says, "Checker variables differ from regular variables in that
they may be both deterministic and nondeterministic. They may have
undefined or partially constrained values, while regular variables are
always deterministic in the sense that they contain only one specific
value at a time." I have not yet finished the proposal, but what does
'undefined' mean here? It seems a little strange

16.8.1 has "The checkers may contain concurrent assertions, checker
variable declarations and assignments, structural procedures, function
declarations, let declarations, sequences and properties, and generate
regions." There is another list on p. 11 in 16.8.2, starting with "A
checker body may contain the following elements:". The lists are not
identical, which is confusing. Better would be to have only one list.
Duplication is a source of inconsistency.

- Re "The following procedures are allowed in a checker (see 16.18.5):
initial_check procedure, encapsulating assertions monitored on the first
clock tick (similar to 16.14.5)". Here is a side issue. 16.14.5 says,
"If the statement appears in an always procedure, the property is always
monitored. If the statement appears in an initial procedure, then the
monitoring is performed only on the first clock tick.
Two inferences are made from the procedural context: the clock from the
event control of an always procedure and the enabling conditions.
A clock is inferred if the statement is placed in an always or initial
procedure with an event control abiding by the following rules:'
It is confusing that the second paragraph does not mention initial
procedures.

16.8.1 has "The checkers may be instantiated where concurrent assertions
may be specified (see 16.14)," followed by a list. The list is not
identical to 16.14's. 'A generate block' does not appear there. (I would
just as soon delete the references to generate blocks, despite Gord's
comment a few months ago). 16.18.3 has yet another list, "Checkers may
be instantiated inside modules, programs, interfaces, and other
checkers".

- The proposal adds the keywords checker and endchecker. endchecker
needs to be added to the list of endxxx keywords created in Mantis 1354.

BNF: Syntax 9-1 shows this:
initial_keyword ::= initial | initial_check4
always_keyword ::= always | always_comb | always_latch | always_ff |
always_check4
4)	It shall be illegal to specify always_check or initial_check
outside of a checker body.
whereas the Syntax in 16.18.2 shows this:
initial_keyword ::= initial2 | initial_check2
always_keyword ::= always2 | always_comb2 | always_latch2 | always_ff2 |
always_check2
2)	initial, always, always_comb, always_latch, and always_ff shall
be illegal in a checker body. initial_check and always_check shall be
illegal outside of a checker body.
They have to be the same. I would do it this way:
initial_keyword2 ::= initial | initial_check
always_keyword2 ::= always | always_comb | always_latch | always_ff |
always_check
2)	initial, always, always_comb, always_latch, and always_ff shall
be illegal in a checker body. initial_check and always_check shall be
illegal outside of a checker body.
Note that I put the footnote reference on the LHS of the production.

New thought: Since these can appear only in checkers and the other
initial and always procedures can only appear outside checkers, why
combine them in the BNF?

Instead of 
checker_or_generate_item ::=
	 { attribute_instance } continuous_assign
	| checker_or_generate_item_declaration
	| initial_construct
	| always_construct
	| concurrent_assertion_item
	| checker_generate_item
initial_construct ::= initial_keyword statement_or_null
initial_keyword ::= initial2 | initial_check2
always_construct ::= always_keyword statement
always_keyword ::= always2 | always_comb2 | always_latch2 | always_ff2 |
always_check2

it might be simpler to do 
checker_or_generate_item ::=
	 { attribute_instance } continuous_assign
	| checker_or_generate_item_declaration
	| initial_check statement_or_null
	| always_check statement
	| concurrent_assertion_item
	| checker_generate_item

- "Each formal argument used in this way may be assigned a value either
in a checker body or in checker action blocks. 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."
The 2nd sentence quoted specifies "written in the checker body". Is the
intent that the following restriction does not apply to formal arguments
assigned in action blocks?

- "The output actual argument shall have a static lifetime." Below, it
says, "Checker actual arguments cannot reference automatic variables."
	("cannot" should be "shall not".) If so, then the first
restriction seems redundant.

- In the example preceding 16.8.4, "end :m" should be "endmodule :m".
- The proposal has examples of the event type used in checker port
lists, such as 
checker my_check (logic test_sig, event clock); 
Since the actual argument connected to this will typically be declared
with a logic data type, where does the LRM say you can connect it to a
formal argument of type event?
- 16.18.6.4 has endsequence : s; There should be no semicolon there. 
- The example has checker check_in_context with a port "logic enable".
The checker instantiation my_check1 connects this port to "en1 ##1 en2".
Is it legal to connect such an expression to a port of type logic? Does
the port need to be untyped? 
- The proposal has the following: 
// Illegal:
// The clock is not inferred from the context,
// it shall be explicitly specified in the checker
// (It is assumed that there is no default clocking declaration
// in the checker declaration scope.)
checker check_illegal (logic test_sig);
property p(logic sig);
...
endproperty
// Illegal: no clock in the property
a1: assert property (p(test_sig));
// Illegal: no clock in the property
c1: cover property (!test_sig ##1 test_sig);
endchecker : check_illegal
"it shall be explicitly specified in the checker" - "shall" is not
appropriate in an example, "must" is better. 
"It is assumed that there is no default clocking declaration in the
checker declaration scope." - "It is assumed" refers only to this
example and not to the general case? It is confusing. 
Most important, it seems to me that the assertions are illegal because
no clock is specified explicitly in the assertion, nor is any inferred
from the context. But this is true of any such property, not just in a
checker, so what is special about this? I guess you want to show that
the clock is not automatically inferred from the instantiation context,
but this is a confusing way to do it. 
- 16.18.2 says that a checker body may contain let declarations, so the
statement in Mantis 1728 that "A let can be declared in any of the
following" needs to be modified to include checkers. 
- 16.18.5 says, "An initial_check procedure may contain concurrent
assertions and event controls only...An always_check procedure may be
specified in the checker body only and may contain concurrent
assertions, nonblocking checker variable assignments (see 16.18.6.1) and
event control statements... The always_check and initial_check
procedures impose the restriction that they contain one and only one
event control and no blocking timing controls." At first it says that
they may contain event controls (plural) and later it says that only one
is allowed. This is confusing. 
- "In the initial_check and the always_check procedures all events from
the explicit sensitivity list of their event control are inferred (if
any specified)," 
The "(if any specified)" is not clear. An event control is required. So
the only alternative to an explicit sensitivity list is an implicit one,
@*. Is that allowed? 


Shalom Bresticker
Intel Jerusalem LAD DA
+972 2 589-6582
+972 54 721-1033

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Tue Feb 5 06:21:45 2008

This archive was generated by hypermail 2.1.8 : Tue Feb 05 2008 - 06:22:03 PST