Subject: [sv-ac] SV-AC 0.79 comments ch 11 - 11.6.8
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Jan 27 2003 - 09:43:08 PST
it can be used wherever sequence_expr appears in the BNF. Cindy asked
Good morning all;
Apologies for missing the meeting.
LRM - In order to better fit the SystemVerilog (and IEEE 1364-2000) documents, I
recommend reversing 11.4 .. 11.10.2 soas to introduce the statements and their context
first, before delving into the interior specifications of the statements themselves.
We must also number examples for ease of discussion and for LRM document.
From SV-EC guidelines on keywords vs. system task calls (my summary is that system tasks
should be preferred for things that would expect to be overridable (pli substitution by
a user, and keywords for everything else.) Thus I would recommend that most of the
system functions be converted to keywords. E.g. $rose, $fell, $stable, $past, $countones
Are we choosing to not support the SV 3.0 system functions, $insetz, $inset, $onehot,
$onehot0, $isunknown() ? Yes, $countones() provides support for the two onehot, but
does not for $inset, $insetz. Also, $isunknown was proposed due to the extreme ease
at writing (a != 1'bx) and the ease at which neither simulation or code reading detects
the code error (and logic error.)
11.2 Second Bassam's thoughts that "check ()" functionality provide limited additional
benefit.
[BNF] - If the action block is defined as "statement_or_null [ 'else' ..."
And statement_or_null is defined as "statement | ';' " then legal syntax
is this:
check (expr) ; ;
When omitting the else statement set. Recommend changing action block to
'statement_or_nothing'
11.3 LRM - Remove text for figure 11-2. It forwardly declares $rose/$fell without
explanations and is not necessary for introduction to concurrent assertions.
11.4 Feel the keyword 'inf' provides little additional benefit to warrant a new keyword.
Suggestions for alternatives: '*', '', ?
Recommend dropping of 'true' as keyword. Verilog to date has not proposed 'true'
or 'false' as keywords. Would want both keywords defined if one is defined.
11.5 Recommend keyword 'sequence' instead of abbreviated keyword 'seq'. This makes
the language consistent in the use of keywords.
All major elements are not abbreviated: module, property, program parameter.
The keyword 'property' is the same number of characters as 'sequence'.
11.6.1 BNF Nonconsecutive repeat syntax contains extra brackets around range. This
would require double brackets " done =* [[ 1:4]].
LRM - Introduction of nonconsecutive syntax needs a heading to separate it from the
previous topic.
11.6.2 LRM - Suggest making Figure 11-4 (and rest of figures) widen the event bar for
greater visibility.
11.6.4 Is the keyword 'intersect' the best to convey "matching with length match" It
does not come across as the best word to describe this idea.
LRM - First bullet of "When there are multiple matches..." says, "a match from the
first operand ... with the same length (end time)."
Well, which is it, the length (of the sequences) must match, or the end time of
the sequence must match with the other sequence? Please note that assertions can
start on subsequent cycles. Thus, one could have an end point, but the length of the
asserition would not be the same.
11.6.6 LRM states "Use the first_match operator when you are interested in only the
first match from a sequence expression that can possibly result in multiple matches."
Suggest rewording as:
"The first match operator matches only the first match of multiple matches of
a sequnce expression from the same starting time."
1. Initial syntax is too casual.
2. Wording does not include fact that sequence may start several times before end
of sequence is reached.
LRM - Add an example waveform figure for this operator.
11.6.7 LRM states "These constructs" replace with singular version.
Strike rest of sentence, "and to select a sequence between two alternatives..."
since this functionality has been removed.
LRM - Should we use the words, "antecedent" and "consequent" in discussing the
implication operator?
LRM - next paragraph, "is a sequence expression that can result in one or match (sic)"
replace "match" with "more".
LRM - 4th paragraph, "Each time a data phase completes..." It states, "matched because
stop gets asserted, while irdy is asserted." The fact that these signals are active
low has been lost and confuses the reader seeing signals fall instead of rise.
LRM (next page) Example of data_end and data_end_rule1 introduces 'ended' before it
is defined. Recommend removal, since with and without the keyword, the result is
the same.
LRM - please spell check the document, next paragraph contains "smatch"
LRM - paragraph after Figure 11-11. Suggest the word 'operator' instead of 'clause'
when talking about the implication operator, "=>".
LRM - last example - several improvements.
1. Can one use non-consecutive repeat instead of seq "s(len)"?
2. s(BLK1) is copied incorrectly instead of s(BLK1), S(BLK2), S(BLK3)
3. the variable 'lp' is not defined - should this be 'len_parm' instead?
11.6.8 LRM Sentence "When the condition is a sequence expression." This is not
complete - strike or rework.
LRM next sentence, "This feature is useful for chaining sequential implication."
I concur with Cindy that this is NOT useful. The example p16 will show my reason.
property p16 = (write_en & data_valid // 1
=> next_event(write_en && retire_address[4:0] == addr) // 2
=> ([3:8] write_en && !data_valid && write_address[4:0] == addr));// 3
Property p16 matches when #1, #2 and #3 occur.
Property p16 fails (if asserted) when #1 and #2 occur and #3 fails - correct?
Property p16 matches when #1 occurs and #2 does not.
Thus if you are really intending to check #3, then you only need to write:
property p16 = (write_en & data_valid;
next_event(write_en && retire_address[4:0] == addr) // 1
=> ([3:8] write_en && !data_valid && write_address[4:0] == addr));// 2
#1 => #2
For another wrong example, see 11.8.
-------------------------------------------------------------------------------------------
THanks.
Adam Krolnik
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Jan 27 2003 - 09:44:49 PST