RE: [sv-ac] New version of 1995 (concurrent asserts in loops) ready for review

Erik,

The sending of this has been delayed, since I am writing it on my plane.
So other people may have already reported some of these issues. 


1. P. 2 says, 
"In a foreach loop, the body shall not modify any dimension of any array
controlling the loop. All controlling arrays shall be non-associative
and have constant bounds."

This 'constant bounds' is not clear to me. Is this just a roundabout way
of saying 'fixed-size'? How could a dynamic array or queue qualify?
Could a bounded queue qualify?


2. "The loop may not contain an early exit using break or continue
constructs." Maybe also the 'disable' construct?


3. In the example

integer [1:0] my_ints = '{123, 456};
always @(posedge clk) begin : b1
	for (i=0; i<=1; i++) begin : b2
	foo[i] = (my_ints[i] == 123);
	a1: assume property (foo[i])
			 $display("Good foo vector: %d", foo[i]);
		else $display("Bad foo vector: %d",foo[i]);
	end
end

For this to display

Bad foo vector: 456
Good foo vector: 123

the $display statements have to display my_ints[i] instead of foo[i].


4. Also, I think 

integer [1:0] my_ints = '{123, 456};

needs to be

integer my_ints [1:0] = '{123, 456};


5. The rewrite at the top of p. 3:

always @(posedge clk) begin
	for (i=0; i<3; i=i+1) begin
		for (j=0; j<=i; j=j+1) begin :
			a1: assert property (foo |-> (bar |->
table[i][j] != `BAD_VAL)));
				else report_failure(i,j);
		end
	end
end
end
end

has an extra colon after the 3rd begin, mismatched parentheses in a1,
and has 2 extra end's.


6. In the sentence,

"The property (foo |-> (bar |-> (table[i][j] != `BAD_VAL:))) will be
evaluated at the
posedge of clk for each legal set of (i,j) values:", 

there is an extra colon after `BAD_VAL.


7. I don't think the rewrite would be equivalent if the original code
would change foo or bar during the execution of the loops or if
something else could change them.


8. Afterwards,

bit [4:0] my_bits = '{0, 1, 0, 0};

defines a 5-bit packed array while the assignment pattern has only 4
elements.

I think you meant

bit [3:0] my_bits = '{0, 1, 0, 0};

and

for (i=0; i<4; i++) begin : b2 // < instead of <=


Thanks,
Shalom
---------------------------------------------------------------------
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, and is
believed to be clean.