Re: [sv-ac] RE: Call to vote: Due September 26

Anupam,
I agree with your position in the need for a concurrent assertion in an
an always_comb.

AP : What if you have something like****

always_comb****

…****

if (a)****

    case(select)****

        ‘b10 : if (b)

  ap1: assert property (@(posedge clk) x ##1 y);****

…****

Do you want this property to be gated only by ‘b’ – if yes, then so you
still keep evaluating the property even when ‘a’ changes to 0 or the value
of ‘select’ changes.

[Ben] The only possibility i to take advantage of the enabling conditions.

Thus, assertion "ap1" would behave as if the always_comb were always_ff
@(posedge clk).

My observation with the simulator is that it did just that. At the clock
edge, all the preconditions are checked before enabling the assertion.

For the always_comb, I think that there is an implicit clock in the
sensitivity list, and that is all that is needed.

Ben

On Fri, Sep 23, 2011 at 10:35 AM, Prabhakar, Anupam <
anupam_prabhakar@mentor.com> wrote:

> Hi Dmitry,****
>
> ** **
>
> I disagree. Please see my comments below.****
>
> ** **
>
> Anupam****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Friday, September 23, 2011 4:27 AM
> *To:* ben@systemverilog.us; Eduard Cerny
> *Cc:* Seligman, Erik; sv-ac@eda-stds.org
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ** **
>
> Hi Ben,****
>
> ** **
>
> Your example does not agree with the position of Ed, Anupam and Manisha.**
> **
>
> ** **
>
> IMO a procedural concurrent assertion should be evaluated at each clock
> tick when its enabling condition is active. In Ben’s example I would expect
> that the new attempt of b |=> d is checked each time when its enabling
> condition a is asserted. Therefore, if a is always 1 this assertion should
> be equivalent to assert property(@ (posedge clk) b|=> d);****
>
> ** **
>
> If we adopt the opposite point of view that the clocking event of the
> concurrent assertion does not belong to the sensitivity list then we will
> have the embedded assertion roughly equivalent to:****
>
> ** **
>
> assert property(@ (posedge clk) $rose(a) |-> b|=> d);****
>
> ** **
>
> which does not seem to be very useful.****
>
> AP : Why do you want to embed a concurrent assertion in an always_comb in
> this case. You can just write it outside the always_comb.****
>
> ** **
>
> Inserting the clocking event into the sensitivity list of the procedure
> should not be very expensive in simulation. The simulator may cache the
> latest value of the context of the concurrent assertion and not to
> reevaluate the entire procedure on the rising edge of the clock, i.e.
> actually not to include the clocking event into the sensitivity list.****
>
> AP : What if you have something like****
>
> always_comb****
>
> …****
>
> if (a)****
>
> case(select)****
>
> ‘b10 : if (b) assert property (@(posedge clk) x ##1 y);****
>
> …****
>
> Do you want this property to be gated only by ‘b’ – if yes, then so you
> still keep evaluating the property even when ‘a’ changes to 0 or the value
> of ‘select’ changes. If not then you would expect the simulator to extract
> all enabling conditions which is not trivial. I have heard this argument
> that embedding a concurrent assertion in an always_comb does not make
> sense. So should we be adding this kind of complexity for a concurrent
> assertion embedded in an always_comb block ? An assertion in true sense
> should be an observer and not a contributor. If you embed a concurrent
> assertion in any procedural block it should only be to trigger its
> evaluation attempt when the execution reaches that point.****
>
> ** **
>
> In fact I don’t mind if we disallow a concurrent assertion inside an
> always_comb block but that would be backward-incompatible.****
>
> ** **
>
> ** **
>
> ** **
>
> ** **
>
> Thanks,****
>
> Dmitry****
>
> ** **
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Wednesday, September 21, 2011 20:13
> *To:* Eduard Cerny
> *Cc:* Seligman, Erik; Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] RE: Call to vote: Due September 26****
>
> ** **
>
> I agree with Ed and Anupa. Below is code that I tested with a simulator.
> In the always_comb, I have: ****
>
> if(a) ****
>
> ap_conc: assert property(@ (posedge clk) b|=> d) else
> $display("ap_coc error");****
>
> The simulator behaved as the following ****
>
> ** **
>
> ap_conc_equivalent: assert property(@ (posedge clk) *if(a)* b|=> d) else
> $display("ap_coc error");****
>
> ** **
>
> module test_abcde; ****
>
> logic clk=0, a=0, b=1, c=1, d=0, e=0; ****
>
> initial forever #10 clk=!clk; ****
>
> ****
>
> // always @ (posedge clk) b <= !b; ****
>
> initial begin ****
>
> #2 e=1'b1; ****
>
> #3 e=1'b0; ****
>
> #7 e=1'b1; ****
>
> #23 b=1'b0;****
>
> #40 b=1'b1; ****
>
> #27 c=1'b0; ****
>
> end ****
>
> ****
>
> always_comb****
>
> begin****
>
> a = b & c;****
>
> ap: assert (a != e) else $display("ap error");****
>
> if(a) ****
>
> ap_conc: assert property(@ (posedge clk) b|=> d) else
> $display("ap_coc error");****
>
> end****
>
> endmodule ****
>
> ** **
>
> Ben Cohen ****
>
> ** **
>
> On Wed, Sep 21, 2011 at 8:46 AM, Eduard Cerny <Eduard.Cerny@synopsys.com>
> wrote:****
>
> I am also a little confused what we are voting on, 2093 or 3564. Regarding
> 3564, my thought is as follows:****
>
> for immediate, deferred and final assertions, only variables in the
> condition of the assertion should contribute to the sensitivity list, not
> those appearing in the action blocks. For concurrent assertions, IMHO they
> should not contribute in any way to the sensitivity list. An attempt is
> enabled when control reaches the location of the assertion in the
> always_comb procedure and then they run totally independently of the always,
> on their own clock. None of the variables in the assertion has anything to
> do with the actual evaluation of the always_comb. ****
>
> ****
>
> Best regards,****
>
> ed****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Seligman,
> Erik
> *Sent:* Wednesday, September 21, 2011 11:34 AM
> *To:* Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> I assume we’re really voting on 3564, not 2093?****
>
> ****
>
> I vote NO on 3564. Reasoning: The current proposal explicitly states
> that expressions in concurrent assertions do not wake up the always_comb,
> but I don’t believe this is a correct solution. As an RTL author, I would
> want the always_comb to wake up at some point soon after any changes to the
> sampled expression, as well as any time a const’ expression changes. ***
> *
>
> ****
>
> Since we agreed that more time is needed for a clean definition of behavior
> under concurrent assertions, we should just talk about immediate assertions
> in this proposal, and leave the concurrent case undefined (which we will fix
> in the next PAR). So I would rewrite the proposal as:****
>
> ****
>
> Expressions used in immediate assertions (see 16.3), within the block or
> within any function called within the block, also contribute to the implicit
> sensitivity list of an *always_comb**. * In the example below, the *always_comb
> *shall trigger whenever b,c or e change.****
>
> ****
>
> *always_comb *****
>
> *begin *****
>
> a = b & c; ****
>
> * assert *(a != e); ****
>
> *end*****
>
> ****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Tuesday, September 20, 2011 11:55 PM
> *To:* sv-ac@eda-stds.org
> *Subject:* [sv-ac] Call to vote: Due September 26****
>
> ****
>
> -You have until 11:59 pm PDT, Monday, September 26, 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 September 20, 2011 meeting, the eligible voters are****
>
> ****
>
> Ashok Bhatt****
>
> Eduard Cerny****
>
> Ben Cohen****
>
> Dana Fisman****
>
> Tapan Kapoor****
>
> Jacob Katz****
>
> Scott Little****
>
> Manisha Kulshrestha****
>
> Anupam Prabhakar****
>
> Erik Seligman****
>
> Samik Sengupta****
>
> Tom Thatcher****
>
> ****
>
> Mantis 2093 ____ Yes ____ No****
>
> http://www.eda-stds.org/mantis/view.php?id=3564 <http://www.eda-stds.org/mantis/view.php?id=2093%20>
> ****
>
> http://www.eda-stds.org/mantis/file_download.php?file_id=5462&type=bug****
>
> ****
>
> ---------------------------------------------------------------------
> 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* <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, and is
believed to be clean.