[sv-ac] RE: Mantis 1995 (asserts in loops)

Hi all--
I have attached the latest draft for comment.
 
Shalom-- I'm still not sure I understand exactly how the example should
be rephrased.  If you could send a few proposed sentences that you would
use to describe it (or a modified example), that would be very useful.
If I understand correctly, I think we're in sync on what the proposed
change is, and the challenge is how to describe it clearly and legally.
 
Thanks!

________________________________

From: Bresticker, Shalom 
Sent: Friday, September 28, 2007 12:10 AM
To: Seligman, Erik
Cc: 'sv-ac@server.eda-stds.org'
Subject: RE: [sv-ac] notes from SV-AC meeting 2007-09-25


As already pointed out, if the foreach begin-end contained a
declaration, then it would not be proper to remove the block name from
it.
 
Shalom


________________________________

	From: Seligman, Erik 
	Sent: Thursday, September 27, 2007 11:40 PM
	To: Bresticker, Shalom; 'john.havlicek@freescale.com'
	Cc: 'sv-ac@server.eda-stds.org'; Korchemny, Dmitry
	Subject: RE: [sv-ac] notes from SV-AC meeting 2007-09-25
	
	
	

	"integer my_ints[2] = {123, 456};
	always @(posedge clk) begin
	  foreach (my_ints[i]) begin : b1
	    foo[i] <= somefunction(my_ints[i]);
	    a1: assume property (foo[i] != `BAD_VAL);
	  end
	end
	
	The assumptions b1[0].a1 and b1[1].a1 in this example are
logically equivalent to the assumptions in the example below:"
	

		[SB] You wrote  "The assumptions b1[0].a1 and b1[1].a1
in this example ".
		But those names do not exist in "this example". You
could talk about the assumptions created on each iteration.

		[ES] Would this phrasing work?:  

		The assumptions generated by this example are logically
equivalent to the assumptions b1[0].a1 and b1[1].a1 in the example
below:

		 

		 


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