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

Dmitry,
I think that in my example the concurrent assertion behaves more like

ap_conc_equivalent: assert property(
    @ (posedge clk) *if(a)* b|=> d) else $display("ap_coc error");
or like
assert property(@ (posedge clk) (a) |-> b|=> d);
I don't think it has the $rose.
The simulator I used seemed to show that behavior, without putting the
clocking in the sensitivity list.
I don't see a harm in putting the clock, or making the behavior as if there
were a clock. Maybe this is what that vendor did.
Ben

On Fri, Sep 23, 2011 at 4:26 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

> 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.****
>
> ** **
>
> 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.****
>
> ** **
>
> 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, and is
believed to be clean.