[sv-ac] RE: Call to vote: Due June 20

Hi Jacob,

Please, see my comments below.

Thanks,
Dmitry

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Katz, Jacob
Sent: Sunday, June 19, 2011 14:58
To: sv-ac@eda-stds.org
Subject: [sv-ac] RE: Call to vote: Due June 20

Mantis 3069 __x__ Yes ____ No

http://www.eda-stds.org/mantis/view.php?id=3069
http://www.eda-stds.org/mantis/file_download.php?file_id=5142&type=bug

Mantis 3033 ____ Yes __x__ No

http://www.eda-stds.org/mantis/view.php?id=3033
http://www.eda-stds.org/mantis/file_download.php?file_id=5152&type=bug

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

[Korchemny, Dmitry] It becomes impractical now to formally define the checker variable assignment, as it becomes almost the same as module variable assignment. To accurate description of the formal semantics of assignments would be huge. Therefore I limited F.3.4.6 to free variable assignment only. The only change in free variable is introduced when their (nonblocking) assignment belongs to a scope of some procedural statement, e.g., a conditional one. To describe this situation I introduced a notion of a Boolean enabling context, in the same way as it is done in the formal semantic of assertion statements.

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?
[Korchemny, Dmitry] The main problem preventing doing that is variable sampling. We have the following rule: everything in always_ff is sampled; everything in always_comb is not. To make the things clear, I am rewriting your example as follows:

logic a, b, c, d;
always @(posedge clk) begin
                logic tmp;
                if (d) begin
                                tmp = some_complex_expression1(a, b);
                ffvar <= tmp & something_else(c);
                end
else begin
                                tmp = some_complex_expression2(a, b);
                ffvar <= tmp & something_else(c);
                end
end

The value of d should be sampled for ffvar, and non-sampled for tmp. The things become confusing. Hence the restriction introduced.

--------------------------------
Jacob M. Katz | jacob.katz@intel.com<mailto:jacob.katz@intel.com> | Work: +972-4-865-5726 | iNet: (8)-465-5726

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Wednesday, June 15, 2011 10:17
To: sv-ac@eda-stds.org
Subject: [sv-ac] Call to vote: Due June 20

-You have until 11.59 pm PDT, Wednesday, June 20, 2011 to respond

-An issue passes if there are zero NO votes and half of the eligible voters respond with a YES vote.

-If you vote NO on any issue, your vote must be accompanied by a reason. The issue will then be up for discussion during a future conference call.

As of the June 14, 2011 meeting, the eligible voters are:

Ashok Bhatt

Laurence Bisht

Eduard Cerny

Ben Cohen

Shaun Feng

Tapan Kapoor

Jacob Katz

Scott Little

Manisha Kulshrestha

Anupam Prabhakar

Samik Sengupta

Tom Thatcher

Mantis 3033 ____ Yes ____ No

http://www.eda-stds.org/mantis/view.php?id=3033
http://www.eda-stds.org/mantis/file_download.php?file_id=5152&type=bug

Mantis 3069 ____ Yes ____ No

http://www.eda-stds.org/mantis/view.php?id=3069
http://www.eda-stds.org/mantis/file_download.php?file_id=5142&type=bug

Below are the changes made in 3069:

- Replaced "global clocking declaration in effect" with "effective global clocking declaration"

- Fixed punctuation and spelling

- Changed
However, any of its instances in the elaborated design description shall contain at most one global clocking declaration. It shall be an error if there is more than one global clocking declaration in a given module, interface, checker or program instance in the elaborated design description.
To
However, any of its instances in the elaborated design description shall contain at most one global clocking declaration; it shall be an error otherwise.

- Changed
When global clocking is referenced in a sequence declaration, a property declaration, or as an actual argument to a named sequence instance, a named property instance, or a checker instance, the point of reference shall be considered after the application of the rewriting algorithm defined in F.4.1, which flattens properties and sequences, and substitutes actual arguments to sequence, property and checker instances for their corresponding formal arguments. As a result, when a property or a sequence declaration containing a reference to global clocking is instantiated in an assertion statement, the hierarchical lookup rules described above shall be applied from the place of the assertion statement appearance in the source description, not from the point of the sequence or the property declaration. Similarly, when global clocking is referenced in an actual argument of a checker instance, the lookup rules shall be applied after the substitution of the actual argument in place of the corresponding formal argument inside the checker body.
To
When global clocking is referenced in a sequence declaration, a property declaration, or as an actual argument to a named sequence instance, a named property instance, or a checker instance, the point of reference shall be considered after the application of the rewriting algorithm defined in F.4.1. As a result, when a property or a sequence declaration is instantiated in an assertion statement, the hierarchical lookup rules described above shall be applied from the place of the assertion statement appearance in the source description, not from the point of the sequence or the property declaration. Similarly, the lookup rules shall be applied after the substitution of the actual argument in place of the corresponding formal argument inside the checker body.

---------------------------------------------------------------------
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<http://www.mailscanner.info/>, and is
believed to be clean.
---------------------------------------------------------------------
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<http://www.mailscanner.info/>, and is
believed to be clean.
---------------------------------------------------------------------
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.