[sv-ac] Review of Draft 6, Sections 16.11--16.14

From: Thomas Thatcher <Thomas.Thatcher_at_.....>
Date: Fri Jun 27 2008 - 10:55:45 PDT
Hello everyone,

Here is a review of Draft 6, Sections 16.11--16.14
I found the following problems:

Tom



16.11:

The following sentence was added by Mantis 2150.  It was assuming the 
implementation of 1995.  The wording of the text may need to change 
because of our changes to the implementation of assertions in procedural 
code.

"The variable passed by value as an input shall be of a type allowed in 
16.6.1. An automatic variable, other than a loop control variable, shall 
not be passed as an argument to a subroutine call either as input or ref 
type. An automatic loop control variable shall be treated like a 
constant when passed as an argument to the subroutine call."


16.12:

I would suggest the following English change to this sentence.  The 
current wording is a little awkward:

REPLACE
An X and Z value of a bit is not counted towards the number of ones.
WITH
A bit with value X or Z is not counted toward the number of ones.


16.13

16.13.4:  There is an extra number in the Section heading:

"6.13.4 1 Conjunction property"


16.13.6:  Implication:

The example and corresponding Figure 16-14 is confusing.
The property data_end is defined as follows:

	property data_end;
	    @(posedge mclk)
	    data_phase |-> ((irdy==0) && ($fell(trdy) || $fell(stop))) ;
	endproperty

The diagram shows that the property evaluates to true at time 6. The 
diagram DOESN'T show that the property evaluates to false at times 
2,3,4,5,7, and 8.  I'm not sure what the property is checking.  Is the 
property checking that all data phases will have a completion?  If so, 
then maybe the property should be written as

	$rose(data_phase) |-> ##[1:10] ((irdy==0) && ($fell(trdy) || 
$fell(stop))) ;


16.13.12: Until Property

I don't think these comments are correct:

	property_expr1 until property_expr2 (weak non-overlapping form)
	property_expr1 s_until property_expr2 (weak overlapping form)
					      ^^^^^^^^^^^^^^^^^^^^^^
	property_expr1 until_with property_expr2 (strong non-overlapping form)
						 ^^^^^^^^^^^^^^^^^^^^^^^^
	property_expr1 s_until_with property_expr2 (strong overlapping form)

Shouldn't  s_until be the strong non-overlapping form, and until_with be 
the weak overlapping form?




16.14.1 Multiclocked sequences

"Differently clocked or multiclocked sequence operands cannot be 
combined with any sequence operators other than ##1. For example, if 
clk1 and clk2 are not identical, then the following are illegal:"

Shouldn't it be   "other than ##0 or ##1"?



16.14.3 Clock flow

"Clock flow eliminates the need to write clocking events in positions 
where the clock is not allowed to change. For example:"

     @(c) x |-> @(c) y ##1 @(d) z

This is implying that the clock can't change across an implication. 
However, the section above was change to define the changing of clock 
across an implication.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Fri Jun 27 10:56:17 2008

This archive was generated by hypermail 2.1.8 : Fri Jun 27 2008 - 10:57:22 PDT