RE: [sv-ac] 16.14.5 Embedding concurrent assertions in procedural code - questions

I think that only immediate assertions should be allowed in final block.
 
ed
 


________________________________

	From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf
Of Seligman, Erik
	Sent: Thursday, September 20, 2007 11:29 AM
	To: Bresticker, Shalom; sv-ac@eda-stds.org
	Subject: RE: [sv-ac] 16.14.5 Embedding concurrent assertions in
procedural code - questions
	
	
	Hi Shalom-- Mantis 1995 and 2005 heavily edit those sections, so
we should probably try to incorporate the fixes you mention with those
items, probably mostly into 2005.  I'll take a closer look & try to
address these issues.  1995 already fixes your last point by eliminating
restriction (c).
	 
	Dmitry, Ed, John-- is there a reason why initial, always, and
final blocks are not treated identically in the lines Shalom mentions?
	 

________________________________

	From: owner-sv-ac@server.eda.org
[mailto:owner-sv-ac@server.eda.org] On Behalf Of Bresticker, Shalom
	Sent: Thursday, September 20, 2007 8:13 AM
	To: sv-ac@server.eda-stds.org
	Subject: [sv-ac] 16.14.5 Embedding concurrent assertions in
procedural code - questions
	
	

	Hi, 

	16.14.5 says (after applying changes from Mantis 1737), 

	16.14.5 Embedding concurrent assertions in procedural code 
	A concurrent assertion statement can also be embedded in a
procedural block. 
	[SB] Can they be embedded in final procedures? 
	... 
	If the statement appears in an always block, the property is
always monitored. If the statement appears in an initial block, 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 block and the enabling conditions.

	A clock is inferred if the statement is placed in an always or
initial block with an event control abiding by the following rules:

	- The clock to be inferred must be placed as the first term of
the event control as an edge specifier (posedge expression or negedge
expression).

	- The variables in expression must not be used anywhere in the
always or initial block. 
	[SB] Not clear. First it says "clock from the event control of
an always block" (always only), then it says, "A clock is inferred if
the statement is placed in an always or initial block " (both always and
initial).

	[SB] What happens if these rules are not fulfilled? Not clear.
Is it illegal? 

	For example: 
	... 
	If the clock is explicitly specified with a property, then it
must be identical to the inferred clock, as shown below: 
	...
	Another inference made from the context is the enabling
condition for a verification statement. Such derivation shall take place
when a verification statement is placed in an if..else block or a case
block.

	The enabling condition assumed from the context is used to
modify the property_expr of the verification statement as follows:

	... 
	The resulting new property_expr then replaces the original
property_expr in the verification statement. A concurrent assertion
embedded in procedural code in an if...else block or a case block
specifies that a new evaluation attempt of the underlying property_spec
begins at every occurrence of the (inferred) clocking event.

	[SB] This last sentence, "A concurrent assertion...", as
modified by Mantis 1737, refers only to the if-else/case situation.
Doesn't it need to be stated as a general statement for embedded
concurrent assertions? Isn't the statement true always?

	... 
	Similarly, the enabling condition is also inferred from case
statements. 
	... 
	The enabling condition is inferred from procedural code inside
an always or initial block, with the following restrictions:

	a) There must not be a preceding statement with a timing
control. 
	b) A preceding statement shall not invoke a task call that
contains a timing control on any statement. 
	[SB] Are these only for if-else/case situations ("The enabling
condition is inferred...") or for all concurrent assertions in
always/initial blocks?

	c) The concurrent assertion statement shall not be placed in a
looping statement, immediately, or in any nested scope of the looping
statement.

	[SB] This is true for all concurrent assertions in
always/initial blocks, isn't it? But it is worded as a restriction on
inferring enable conditions in if-else/case statements. But if the
assertion is not embedded in an if-else/case, what then? If the
restriction is always, it should be placed unconditionally.

	Thanks, 
	Shalom 


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

	
---------------------------------------------------------------------
	Intel Israel (74) Limited
	
	This e-mail and any attachments may contain confidential
material for
	the sole use of the intended recipient(s). Any review or
distribution
	by others is strictly prohibited. If you are not the intended
	recipient, please contact the sender and delete all copies.

	-- 
	This message has been scanned for viruses and 
	dangerous content by MailScanner <http://www.mailscanner.info/>
, and is 
	believed to be clean. 
	-- 
	This message has been scanned for viruses and 
	dangerous content by MailScanner <http://www.mailscanner.info/>
, and is 
	believed to be clean. 


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