RE: [sv-ac] RE: 2804 proposal uploaded

Hi Erik,
 
The reason for the confusion here is that in (b) it says "there is
exactly one event control in the procedure". So, should the clocking
events used in the assertions and other related places in the procedural
code be considered 'event control' ? In assertions chapter we use term
'clocking event' for the assertions. Probably we need to include term
'clocing event' in this statement. And an example will definitely help.
 
Thanks.
Manisha

________________________________

From: Seligman, Erik [mailto:erik.seligman@intel.com]
Sent: Monday, June 07, 2010 8:27 PM
To: Kulshrestha, Manisha; Eduard Cerny; Korchemny, Dmitry
Cc: sv-ac@server.eda.org
Subject: RE: [sv-ac] RE: 2804 proposal uploaded

Manisha-I think the language is clear, in that no exceptions are
provided: so absolutely any use as an event control within the
procedure is OK. So in your example below, the use of the clk in
$sampled is fine, and does not prevent clock inference.

Can you come up with a real-life example where a signal is used as an
event control in a procedure, and that use should invalidate inference
of that signal as a potential clock? My thought was that in the
common cases I can think of, if someone uses the signal in an event
control, it's because they consider it to be a clock.

Perhaps in addition to fixing the language we should add some examples
to the LRM, like what you have below, to clarify.

From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Monday, June 07, 2010 5:29 AM
To: Seligman, Erik; Eduard Cerny; Korchemny, Dmitry
Cc: sv-ac@server.eda.org
Subject: RE: [sv-ac] RE: 2804 proposal uploaded

Hi Erik,

I am not sure if the language 'in such a way as to affect the state of
the variables assigned in the procedure, other than as an event
control.' is clear enough to handle all the cases we had earlier. How
about this example (just a random one):

reg tmp_a;

.....

always @(posedge clk)

begin

  tmp_a = $sampled(b, @(posedge clk));

  $display($time, ": sampled value of a is %b", tmp_a);

  assert property (a);

end

When we say 'as an event control', is it referring to event control of
the always block or it means any event control (including the event
expressions used in assertions or sampled value functions etc.) ? I feel
this statement is kind of open ended and different tool vendors will end
up interpretting it differently.

Manisha

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Seligman, Erik
Sent: Saturday, June 05, 2010 3:06 AM
To: Eduard Cerny; Korchemny, Dmitry
Cc: sv-ac@server.eda.org
Subject: [sv-ac] RE: 2804 proposal uploaded

I have uploaded another attempt at this proposal, to the Mantis at
http://www.verilog.org/mantis/view.php?id=2804 .

The language for part 1 still sounds a little awkward, and improvements
are welcome. I wanted to make sure it applies to both these cases in
checkers:

checker c1 (event ev1, event ev2)

always @(ev1)

   ... // always infer ev1 controlling assertions here since event
control is single variable

always @(ev1 or ev2)

   ... // Might be able to infer here if either ev1 or ev2 uniquely
meets the conditions in the rule after the actual value is substituted

      // For example, maybe ev1 = "posedge clk", ev2 = "negedge rst",
etc.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Seligman, Erik
Sent: Thursday, June 03, 2010 7:54 AM
To: Eduard Cerny; Korchemny, Dmitry
Cc: sv-ac@server.eda.org
Subject: [sv-ac] RE: 2804 proposal uploaded

Yes-I think according to our simple convention of always inferring if
it's an event variable, we should always infer in your example to be
consistent. I think this would mean I need to change some phrasing
slightly.

On the iff issue, I don't have strong feelings either way. My
inclination would be to allow inference if a gated clock in the presence
of an iff... does somebody agree or disagree?

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Thursday, June 03, 2010 6:49 AM
To: Korchemny, Dmitry; Eduard Cerny; Seligman, Erik
Cc: sv-ac@server.eda.org
Subject: RE: 2804 proposal uploaded

Hi Dmitry,

I think that in checkers it should infer always, never mind the form of
the clocking event. Since checkers are special units, presumably whoever
wrote them knew what she/he was doing.

Best...

ed

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Thursday, June 03, 2010 8:25 AM
To: Eduard Cerny; Seligman, Erik
Cc: sv-ac@server.eda.org
Subject: RE: 2804 proposal uploaded

Hi Ed, Erik,

Yes, you are right about clocking blocks and checkers. One more
question: should we disallow iff clause for (clocking block) events?
Also, are formal arguments of type event are considered event variables?
If yes, there is an ambiguity in checkers: on one hand the formal event
should always be inferred, on the other hand, it should only be inferred
upon argument substitution. I am talking about the following case:

checker check (x, event clk);

always @clk

                a1: assert property(x): // Should @clk be inferred here?

endchecker

module m(logic a, clock,...);

...

check c(a, clock)

endmodule

Thanks,

Dmitry

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Eduard Cerny
Sent: Thursday, June 03, 2010 3:11 PM
To: Korchemny, Dmitry; Seligman, Erik; Eduard Cerny
Cc: sv-ac@server.eda.org
Subject: [sv-ac] RE: 2804 proposal uploaded

Hi Dmitry,

I think that the other issues are covered by the other conditions in
Erik's proposal, no?

ed

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Thursday, June 03, 2010 3:50 AM
To: Seligman, Erik; Eduard Cerny
Cc: sv-ac@server.eda.org
Subject: RE: 2804 proposal uploaded

Hi

I agree with this statement. I would add a clarification that the tool
is required to detect dependency only in the scope to which the always
procedure belongs. Also, addressing clock inference of the form @clk in
checkers or when clk is a clocking block event is not covered by this
statement.

Thanks,

Dmitry

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Seligman, Erik
Sent: Wednesday, June 02, 2010 6:11 PM
To: Eduard Cerny
Cc: sv-ac@server.eda.org
Subject: [sv-ac] RE: 2804 proposal uploaded

Hi guys-Ed has a suggestion that rather than the ugly list of categories
for exempting a signal appearance for clock inference, we do something
like this:

No term in expression1 appears anywhere else in the body of the
procedure in such a way as to affect the state of the variables assigned
in the procedure, other than as an event control.

What do you think? Would this work?

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Wednesday, June 02, 2010 8:07 AM
To: Seligman, Erik
Subject: RE: 2804 proposal uploaded

Hi Erik,

the first part is just the tail of your sentence starting from task
instance. But If we use the 2nd form that part would not be needed.
Perhaps the 2nd point could be modified to say "not affect other than by
the even control"?

best...

ed

From: Seligman, Erik [mailto:erik.seligman@intel.com]
Sent: Wednesday, June 02, 2010 10:36 AM
To: Eduard Cerny; Korchemny, Dmitry
Subject: RE: 2804 proposal uploaded

I'm not sure I understand your first point-can you re-specify the full
sentence as you would change it?

For the second point, I don't think your rephrasing would work...
wouldn't the use as a clock within the procedure potentially affect the
state of variables?

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Wednesday, June 02, 2010 6:24 AM
To: Seligman, Erik; Korchemny, Dmitry
Cc: Eduard Cerny
Subject: RE: 2804 proposal uploaded

Hi Erik

regarding

task instantiation, or system function or task.

should it be the actual arguments to a task, system function or system
task call?

Still, what about:

No term in expression1 appears anywhere else in the body of the
procedure in such a way as to affect the state of the variables assigned
in the procedure.

best regards,

ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Seligman, Erik
Sent: Tuesday, June 01, 2010 6:03 PM
To: Korchemny, Dmitry; sv-ac@server.eda.org
Subject: [sv-ac] 2804 proposal uploaded

Hi guys-I have uploaded a new proposal at
http://www.verilog.org/mantis/view.php?id=2804, which I think captures
the results of this morning's discussion. Please take a look & comment
if further changes are needed.

-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
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 <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.