[sv-sc] Mantis 1648, 2091, and 2100, Also 19.9-19.12

I agreed to review these mantis items to see if they need to be changed
as a result of yesterday's discussions.  Here are the results.

D5 Chapter 19.9-19.12:  No changes needed. There are no references to
assertions in procedural code.

========================================================================

Mantis 1648: Default disable iff:  There is one example that may need
clarification. I am thinking it would be best to simply reference the
new section that talks about inferred enabling conditions:

In 16.15 Disable iff resolution, change:

		// Only enable condition and clocking event are inferred
from an always
		block
		// Assertion a8 is equivalent to
		// assert property (@(posedge clk) !bit'(rst!='b0) |->
(a |=> b));
		always @(posedge clk or posedge rst)
		if (rst)
		   ...
		else begin
		   a8 : assert property (a |=> b);
		   ...
		end

In assertion a8 the inferred enabling condition is from the else clause
of the if-else statement, and thus
it has to represent the complementary interpretation of the four-valued
expression in the if condition. One
such form is as indicated in the comment above a8. Other equivalent
forms may be used, such as ((rst !=
'b0) !== 1'b1).

to:

		// Only enable condition and clocking event are inferred
from an always
		block
		// Assertion a8 is equivalent to
		// assert property (@(posedge clk) !bit'(rst!='b0) |->
(a |=> b));
		always @(posedge clk or posedge rst)    /* NOTE TO
EDITOR: Notice new indentation of if-else*/
		    if (rst)
		       ...
		    else begin
		       a8 : assert property (a |=> b);
		       ...
		end

In assertion a8 the inferred enabling condition is from the else clause
of the if-else statement, and thus
it has to represent the complementary interpretation of the four-valued
expression in the if condition. One
such form is as indicated in the comment above a8. Other equivalent
forms may be used, such as ((rst !=
'b0) !== 1'b1).  Refer to section <insert reference and link here> for
more details on inferred enabling conditions.
		
		
======================================================================
Mantis 2091: where concurrent discussions can be placed: 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.

 Change in 16.4 Concurrent Assertions Overview:    

Concurrent assertions describe behavior that spans over time. Unlike
immediate assertions, the evaluation model is based on a clock so that a
concurrent assertion is evaluated only at the occurrence of a clock
tick.  The values of variables used in the evaluation (except for the
special case of loop iterators as described in 16.14.5) are the sampled
values. This way, a predictable result can be obtained from the
evaluation, regardless of the simulator's internal mechanism of ordering
events and evaluating events. This model of execution also corresponds
to the synthesis model of hardware interpretation from an register
transfer language (RTL) description

To:
Concurrent assertions describe behavior that spans over time. Unlike
immediate assertions, the evaluation model is based on a clock so that a
concurrent assertion is evaluated only at the occurrence of a clock
tick.  The values of variables used in the evaluation (except for the
special case of loop iterators as described in 16.14.5) are the sampled
values.  Variables in a concurrent assertion use the value sampled in
the Preponed region of a time slot with the following exceptions:
-	exception that local variables use the current value
-	and for and foreach loop variables iterators use the current
value.(see 16.14.5)
-	enabling conditions that are inferred from procedural code use
the current value 

This way, a predictable result can be obtained from the evaluation,
regardless of the simulator's internal mechanism of ordering events and
evaluating events. This model of execution also corresponds to the
synthesis model of hardware interpretation from an register transfer
language (RTL) description

Also delete the subsequent sentence in 16.4 Concurrent Assertions
Overview

All variables in a concurrent assertion use the value sampled in the
Preponed region of a time slot with the exception that local variables
and for and foreach loop variables use the current value

=====================================================================
Mantis 2100: synchronous resets:  No changes required.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.