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

(b[->1], v=e)[*m] would work nicely.
Thanks,
Ben

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

> On a second thought, same could be written slightly shorter as****
>
> (b[->1], v=e)[*m]****
>
> No?****
>
> ** **
>
> Dana****
>
> ** **
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Wednesday, December 21, 2011 11:07 AM
> *To:* Dana Fisman Ofek
> *Cc:* Little, Scott; sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* 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.