[sv-ac] Email ballot result (August 8)

Below are the results of the email ballot:

2578 3033
Ashok Bhatt
Yes Abstain Laurence Bisht
Yes Yes Eduard Cerny
Yes Yes Ben Cohen
Tapan Kapoor
Jacob Katz
Yes Abstain Scott Little
No No Manisha Kulshrestha (sent late)
Yes Yes Anupam Prabhakar
Yes Yes Erik Seligman
Samik Sengupta
Yes Yes Tom Thatcher

Issue 2578 passed: 7y/0n/0a with friendly amendments. One negative vote sent late.
Issue 3033 failed: 5y/0n/2a. One negative vote sent late.

Comments

Ed

2578
Minor correction - add s (shown is green):
and the evaluation attempts of property_expr1 is nonvacuous and property_expr2 are nonvacuous.

3033
In REPLACE in 17.3.1

the new example uses "always" rather than always_ff. But always was eliminated from checkers.

similarly in 17.7.1 Checker variable assignments
and Example 2

Should F.3.4.6 also have always_ff or here it does not matter?

Erik

3033
Friendly amendments:

- p.9, example: check_outside is missing an arg

- p.15, 1st bullet point: "In always_ff procedure" ==> "In always_ff procedures"

- C.2.7: Rephrase 1st paragraph: "The always procedure allowed by IEEE Std 1800-2009 in checkers, but always_comb, always_latch, and always_ff were forbidden. The limitations imposed on the always procedure in checkers included the limitations imposed on always_ff procedures outside checkers. In this version of the standard always_comb, always_latch, and always_ff have been added for checkers. As a result the general always procedure in checkers would have imposed the same limitations as always_ff does. Therefore the usage of always procedures in checkers is deprecated and does not appear in this version of the standard."

Also, a question about 17.3. Since we're adding a new limitation on checkers containing procedural code, is it important for us to include an example with a deferred assertion outside a procedure, and point out how its implicit always_comb prevents its checker from being instantiated by other checkers?

Ben

3033
Friendly amendment:
1) Example is missing an "end" statement for the module m
2) The model needs to be beautified -- below is a copy that does it

module m(input logic rst, clk, logic en, logic[7:0] in1, in2,
        in_array [20:0]);
    c1 check_outside(posedge clk, in1);
    always @(posedge clk) begin
        automatic logic [7:0] v1 = 0;
        if (en) begin
            // v1 is automatic, so current procedural value is used
            c1 check_inside(posedge clk, in1, v1);
        end
        for (int i = 0; i < 4; i++) begin
            v1 = v1 + 5;
            if (i != 2) begin
                // v1 is automatic, so current procedural value is used
                c1 check_loop(posedge clk, in1, in_array[v1]);
            end
        end
    end
endmodule : m

3) Change "if (rst) z <= b; // sampled value of rst" TO
    if (rst) // sampled value of rst
hecker check(logic a, b, c, clk, rst);
                logic x, y, z, v, t;
                assign x = a; // current value of a
                always_ff @(posedge clk or negedge rst) // current values of clk and rst
                begin
                                a1: assert (b); // sampled value of b
                                if (rst) z <= b; // sampled value of rst
                                                z <= b; // sampled value of b
                                else z <= !c; // sampled value of c

Scott
3033

I am not going to have enough time to properly review this proposal

Tom
3033

Friendly amendments:

17.3 Checker instantiation

Include the entire paragraph in the change. It's much easier to find the context that way.

Was there a reason for adding the restriction on instantiating a checker

  containing procedural code?

17.3.1

Change:

For instance check_outside,

To

For checker instance check_outside,

In reading the proposal, I kept interpreting this as "for example"

Additional Comment:

I think we did determine that a sequence triggered() method would be

legal in an always_ff:

     always_ff @(sequence.triggered()) begin

         cg.sample()

     end

But it still feels more natural to write it as an always block rather

than an always_ff.

Anupam

3033

Friendly amendment
I think you should change
if (rst) z <= b; // sampled value of rst
to
                if (const'(rst)) z <= b; // using const cast to get current value of rst

for this to me meaningful - this also conveys the message that sampled value will be read otherwise.

Laurence
2578

and the evaluation attempt of property_expr1 is nonvacuous and property_expr2 is nonvacuous.
I consider the following as an expression (property_expr1and property_expr2).

3033
Network error - seems the site is down

Manisha
2578
The sentence "and the evaluation attempt of property_expr1 is
nonvacuous and property_expr2 are nonvacuous." Does not look right. Shouldn't the word 'attempt' be plural ?

3033
Need more time to review
---------------------------------------------------------------------
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.