Re: [sv-ac] Make (b, v = e)[->2] legal in next 201X version?

Dana and Scott,
Thanks for your comments. This is what I want
 (b[->1] ##0 (1, v=e))[*m]
Thus, the VGLD example could be rewritten as:

   property p_fifo_rd_too_short_check;
      logic [3:0] v_length;
      @(posedge clk) ($rose(enable), v_length=length) |->
         enable throughout
         (fifo_rd[->1] ##0 (1, v_length=v_length-1'b1)) [*0:$]
         ##1 v_length==0;
   endproperty : p_fifo_rd_too_short_check
Thanks again,
Ben

On Wed, Dec 21, 2011 at 7:47 AM, Dana Fisman Ofek
<Dana.Fisman@synopsys.com>wrote:

> Hi Ben, Scott,****
>
> ** **
>
> I believe (b[->m], v=e) is different than what Ben wanted.****
>
> I guess, though, (b[->1] ##0 (v=e))[*m] is. ****
>
> It’s not that simple, but perhaps better let one use it, then add rewrites
> with controversial unwrappings.****
>
> ** **
>
> Dana****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Little,
> Scott
> *Sent:* Wednesday, December 21, 2011 10:40 AM
> *To:* ben@systemverilog.us; sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* RE: [sv-ac] Make (b, v = e)[->2] legal in next 201X version?***
> *
>
> ** **
>
> Hi Ben,****
>
> ** **
>
> It seems like your rewrite isn’t quite equivalent. Annex F defines the
> equivalence as:****
>
> ** **
>
> b[->m] == (!b [*0:$] ##1 b)[*m]****
>
> ** **
>
> A sequence of b with length m would satisfy the goto and the above
> rewrite. I believe that your rewrite requires an alternation of b and !b.
> ****
>
> ** **
>
> The syntax (b[->m], v=e) is legal. Does that not do what you want?****
>
> ** **
>
> Thanks,****
>
> Scott****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Tuesday, December 20, 2011 8:48 PM
> *To:* sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* [sv-ac] Make (b, v = e)[->2] legal in next 201X version?****
>
> ** **
>
> In reference to:
> http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=4356
> ****
>
> The following is currently illegal in SVA: ****
>
> (b, v = e)[->2] ****
>
> as that is equivalent to: ****
>
> ((!b, v = e)##[0:$](b, v = e))[*2]****
>
> and the update of v when !b==1 is not desired. ****
>
> ** **
>
> Question to this group: Do we want in the next LRM update to allow such
> a structure****
>
> (b, v = e)[->2] , but with the definition that it be equivalent to: ****
>
> ((!b)##[0:$](b, v = e))[*2] , meaning that the sequence match item is
> only updated when there is a match of the variable. ****
>
> ** **
>
> Do you feel that this is important? ****
>
> Ben Cohen ****
>
> ** **
>
> A bit more info about the rule: The consecutive repetition operator can be
> applied to general sequence expressions, but the goto repetition and
> nonconsecutive repetition operators can be applied only to boolean
> expressions. In particular, goto repetition and nonconsecutive repetition
> cannot be applied to a boolean expression to which a sequence match item
> has been attached. For example,****
>
> *Code:*****
>
> // the following is a legal sequence expression:
> (b[->1], v = e)[*2]
> // but the following is illegal:
> (b, v = e)[->2]****
>
>
> --
> 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.