[sv-ac] Mantis 1900 comments - Part 1

Comments on Mantis 1900:

- The Objectives section says, "Modules are always assumed to contain
design code that is synthesizable into silicon". This is only an
introduction to the proposal, but 'always' is not correct. How about
'often'?

- In 16.3.6, "persists through the Observe region" should be "Observed
region".

- "It shall be considered an error if this method is used in disable iff
boolean expression for properties." Add "the" before "disable iff".

- 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".

- "A sequence treats its formal argument as a local variable if the
formal argument is used as an lvalue in operator_assignment or
inc_or_dec_expression in  sequence_match_item. "
I would add helper words: "A sequence treats its formal argument as a
local variable if the formal argument is used as an lvalue in an
operator_assignment or inc_or_dec_expression in a sequence_match_item. "

- 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.

- "non-blocking" should be without hyphens, several times.

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

- 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.

Enough for one day.

Regards,
Shalom

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.