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

Hi Shalom-- thanks for the comments.  See my followup questions below.


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?

Yes, fixed-size is what I meant.   Is that a better term to use here
than 'constant'?

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

Good point, I'll add that.


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].

Oops, obviously I mixed up a couple of examples.  Will fix.


4. Also, I think

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

needs to be

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

Will fix.


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.

Will fix.


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.


Will fix.



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.


Actually, I think it would be-- if I understand right, as we have
assertions in procedural 'if' statements defined now, the assertion
would just use the sampled values of foo and bar anyway.  So
intermediate values during the procedural code would not actually affect
it.  



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 <=




Will fix.

 

 


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