[sv-ac] E-mail ballot results 6/20/2011

                        Mantis 3033 Mantis 3069

Ashok Bhatt
Laurence Bisht
Eduard Cerny
Ben Cohen n y
Shaun Feng n y
Tapan Kapoor
Jacob Katz n y
Scott Little n y
Manisha Kulshrestha n y
Anupam Prabhakar
Samik Sengupta
Tom Thatcher n y

Mantis 3069 Passed: No Friendly amendments

Mantis 3033 Failed: Comments:

Ben:

Why were the statements about sequences and properties deleted?
Nothing is mentioned about the handling of sequences and properties as
arguments.
Consider the following example:

Tom:

17.5 example
     always_latch
         if (clk) // current value of clk
           t<=b; // current value of b

It appears the only way to make a latch work in a checker is to
explicitly sample it's input
     always_latch
         if (clk) // current value of clk
           t<=$sampled(b); // Need to explicitly sample

17.5 "The reason for sampling expressions in always and always_ff
procedures is to make checkers behave deterministically.

The language should be changed because it is not really correct. The
code in the example will behave deterministically, even if there is no
sampling on a. The behavior, however is not the desired behavior. The
variable a would be assigned in the Active region, and the assignment in
the checker always block would always pick up the new value. There is
only one case that would behave indeterministically. This would occur
when variable a is assigned with a blocking assignment from test bench
code (bad coding style). In this case, the result would depend on
whether the assignment to a was processed first, or this always block
was processed first. A properly coded test bench would use a
non-blocking assignment to a, and the result would be perfectly
deterministic.

What we really want to say here is that variables need to be sampled
because it gives the desired behavior when working with design variables
that are assigned in the Active or NBA regions. i.e. we want an
always_ff to act like a flip-flop!

--- In always and always_ff procedures, only nonblocking assignments are
allowed . . .

Do we need an example for this? This is a fairly straightforward rule.
  At least make the example shorter.

Shouldn't always_latch be included in this?

--- The right hand side of continuous and blocking procedural
assignments shall not contain free variables

Why not?

Are you going to have a complementary rule for always_comb? i.e. only
blocking assignments?

Jacob:

1. Shouldn’t F.3.4.6 be updated with the newly allowed forms of
assignments?

2. Why don’t we allow blocking assignments in always_ff? In
modules this is handy, for example, for variables that are defined
inside the procedural code and hold temporary computation results, e.g.:

logic a, b, c, d;

always @(posedge clk) begin

                 logic tmp;

                 if (d)

                                 tmp = some_complex_expression1(a, b);

                 else

                                 tmp = some_complex_expression2(a, b);

                 ffvar <= tmp & something_else(c);

end

This way the computation may be decomposed into several simpler steps,
without the need to write a separate always_comb or writing unreadable
expressions on the RHS of the assignment to ffvar. This is not a bad
coding style and does not cause any non-determinism. Can it be allowed
in checkers, possibly on the expense of more complex sampling rules?

This issue becomes especially confusing considering the fact that the
following code using a function is legal according to the proposal,
while the one above is not:

function logic foo(input c1, e1, e2, e3);

                 logic tmp;
                 if (c1)
                                 tmp = some_complex_expression1(e1, e2);
                 else
                                 tmp = some_complex_expression2(e1, e2);
                 return something_else(tmp, e3) :
endfunction

logic a, b, c, d;
always @(posedge clk) begin
                 ffvar <= foo(d, a, b, c);
end

The only difference between the two examples is that the call to foo()
is “inlined” in the former…

In general, I believe the “synthesizability” rules for the usual code in
modules only requires that there is no mixture of blocking and
non-blocking assignments to the same variable, plus the
single-assignment-rule. This probably means that formal semantics may be
defined for code that obeys such rules. If so, why do we need more
severe limitations for code in checkers? Or am I missing something?

Manisha:
I need more time to review this proposal. The last proposal on sampling
had a reference about sampling of checker actual arguments. That should
be fixed now. Also, now since sampling is discussed in this proposal for
different types of procedual blocks, it should be made clear that
concurrent assertions use sampled values irrespective of where they are.
Also, if there is a deferred or simple immediate assertion in always
block, does it use sampled value or current value ?

Scott:
I haven’t had time to thoroughly review the proposal, but I do have some
questions/suggestions.

1. If always behaves exactly like always_ff in checkers why allow always
in checkers? Is it only for backward compatibility? To me, it seems
odd to have a restricted form of always in checkers that is exactly the
same as another available construct.

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