Re: [sv-ac] RE: Open Mantis items // Mantis 3195

Dana,.
From what you are saying, each thread caries a copy of the local variables,
and unless a variable is *free*, the variables from each thread must have
the same values at all cycles of the concurrent threads. To obviate this
requirement of *same value, *you can *free *a local variable within a
thread. If understand this correctly, a *free*d local variable cannot be
assigned (?), or if it is, it no longer becomes free(?). If a freed
variable is assigned can it be read within the thread, and discarded when
joined with an intersect?

The issue with SVA is backward compatibility. The "automatic" declaration
of local variable allows for backward compatibility.
Ben Cohen

On Tue, Mar 22, 2011 at 12:52 AM, Dana Fisman <Dana.Fisman@synopsys.com>wrote:

> Hi Ben,
>
>
>
> Yes, the idea in PSL is that intersection is plain intersection also when
> local variables are in the picture. Thus, if a local variable v appears in
> both branches of *intersect* it should have the same value *throughout* in
> *each* of the cycles.
>
> So in
>
> (!a[*] ##1 *(*(a,v++) ##1 !a[*]*)[*]*) intersect (!b[*] ##1 *(
> *(b,v++) ##1 !b[*]*)[*]*)
>
> the a’s and b’s should occur at exactly the same time (as otherwise v will
> change differently in each of the branches).
>
> And
>
> (!a[*] ##1 *(*(a) ##1 !a[*]*)[*]*) intersect (!b[*] ##1 *(*(b,
> v++) ##1 !b[*]*)[*]*)
>
> will not be matched if there is at least one b.
>
>
>
> Since this may not be what one wants, a local variable can be *free*d in a
> certain sequence, this means that it can take any value there.
>
> So that
>
> (free(v) !a[*] ##1 *(*(a) ##1 !a[*]*)[*]*) intersect (!b[*] ##1
> *(*(b,v++) ##1 !b[*]*)[*]*)
>
> can be matched on the same traces as the sequence (!a[*] ##1 (a ##1
> !a[*])[*]) intersect (!b[*] ##1 (b ##1 !b[*])[*]) is, and v will hold the
> number of b’s in that trace.
>
>
>
> Now you can “read” a local variable that is “written” in a parallel branch.
> For instance,
>
> (free(v) !a[*] ##1 *(*(a && v%2==0) ##1 !a[*]*)[*]*) intersect
> (!b[*] ##1 *(*(b,v++) ##1 !b[*]*)[*]*)
>
> will be matched by traces where a’s occur between an even occurrence of b
> to an odd one.
>
>
>
> Dana
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Tuesday, March 22, 2011 12:57 AM
> *To:* Dana Fisman
> *Cc:* Korchemny, Dmitry; sv-ac@eda-stds.org
>
> *Subject:* Re: [sv-ac] RE: Open Mantis items
>
>
>
> Dana,
>
> Are you proposing something like:
>
> property P3; // Current SVA with error
>
> logic v1, v2;
>
> (($rose(a), v1=1) ##1 (b)) and
>
> (($rose(c), v2=0) ##1 (d) && v1) |-> e ;
>
> // local variable v1 referenced in expression where it does not flow.
>
> endproperty : P3
>
> aP3: assert property(@ (posedge clk) P3);
>
>
>
> property P3; // Proposed SVA
>
> logic v1, v2;
>
> (*free *(v2) ($rose(a), v1=1) ##1 (b)) and
>
> (($rose(c), v2=0) ##1 (d) && *v1*) |-> e ; // ??
>
> endproperty : P3
>
> aP3: assert property(@ (posedge clk) P3);
>
>
>
> Actually, the PSL does not seem to address (or show an example of) the
> assignment of a local variable in one sequence that is ANDed with another
> sequence that reads that local variable.
>
>
>
> From the PSL LRM: The free operator when applied to a local variable
> removes the variable from the current scope.
>
> ..
>
> A local variable is visible in the SERE or property in which it is declared
> and in any sub-SERE or sub-property of the SERE or property in which it is
> declared, except if it has been freed using the free operator.
>
> ..
>
> always ([[ reg [31:0] count_r<= 32’d0; reg [31:0] count_w<= 32’d0; ]]
>
> { {fifo_empty;
>
> { free(count_w) read_req[->][[count_r<=count_r+32’d1;]][*];
>
> !read_req[*]} &&
>
> { free(count_r) write_req[->][[count_w<=count_w+32’d1;]][*];
>
> !write_req[*]};
>
> fifo_empty }} |-> {count_r==count_w})
>
>
>
> On Mon, Mar 21, 2011 at 6:36 AM, ben cohen <hdlcohen@gmail.com> wrote:
>
> Dana,
>
> So, what do you propose? That we do something like PSL? Your last sentence
> was cut off.
>
> I am open to any idea.
>
> Q for Dmitry: Can I join the call tomorrow to discuss this?
>
> Ben
>
>
>
> On Mon, Mar 21, 2011 at 1:40 AM, Dana Fisman <Dana.Fisman@synopsys.com>
> wrote:
>
> Hi Ben,
>
>
>
> I looked at your proposal. I understand the motivation behind, but I don’t
> think any new machinery is needed to get what you want. More precisely, if
> we align to the PSL semantics I believe we can address this for free.
>
>
>
> Let me explain the main difference in the semantics of local variables in
> SVA and PSL. The issue both semantics are trying to overcome has to do with
> the sequence operators intersect/and/or which are perceived as parallel
> threads. Then questions such as “can a local variable have different values
> in different parallel threads?”, and “what should the value be after the
> threads unite back?” arise.
>
>
>
> In SVA the semantics of sequences looks at the value of local variables
> only at the beginning and end of a match of a sequence. To overcome the
> above issues (A) special functions (flow\block\sample) are used to
> determine the value of local variables when the threads unite, and (B)
> syntactic restrictions are imposed so that controversial scenarios are
> disallowed.
>
>
>
> In PSL the semantics of sequences looks at the value of local variables at
> all cycles of the match (rather than just at the beginning and end) as is
> the case for any other (non-local) variable. As a result no change is needed
> for or and intersect -- they are plain union and intersection. Moreover no
> syntactic restrictions are imposed.
>
>
>
> Now let’s interpret the examples in your proposal as in PSL. It seems to me
> t
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Thursday, March 17, 2011 5:28 PM
> *To:* Korchemny, Dmitry
> *Cc:* Dana Fisman; sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] RE: Open Mantis items
>
>
>
> On 3195, I uploaded a tentative, non-formal proposal. It is available at
> http://bit.ly/gMewk9
>
> and in attached file Anextensionforlocalvariables.pdf at
>
> http://www.eda-stds.org/svdb/view.php?id=3195
>
>
>
> Ben Cohen
>
>
>
> On Wed, Mar 16, 2011 at 12:10 AM, Korchemny, Dmitry <
> dmitry.korchemny@intel.com> wrote:
>
> Hi Dana,
>
>
>
> 3057 is a pure syntactical proposal and it is independent from other two.
> If somebody is willing to address 3195, he/she can also address 3059. We can
> discuss it next time. The freeze date is September-October 2011.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* Dana Fisman [mailto:Dana.Fisman@synopsys.com]
> *Sent:* Wednesday, March 16, 2011 09:03
> *To:* Korchemny, Dmitry; 'sv-ac@eda-stds.org'
> *Subject:* RE: Open Mantis items
>
>
>
> Hi Dmitry,
>
>
>
> I would like us to reconsider the recommendation given for item regarding
> local variables. The current recommendation is:
>
>
>
> 3057
>
> WIP
>
> Make local variables a first class language construct in SVA.
>
> 3059
>
> Postpone
>
> Study PSL local variables and determine if any alignment is warranted.
>
> 3195
>
> Address if feasible
>
> Local Variables Flow Out Issue in and/or/intersect/implies
>
>
>
> I believe the 3 items are closely related. In PSL local variables are first
> class constructs, and there are no flow out issues with
> and/or/intersect/implies. So perhaps we can tackle all at once and get a
> satisfactory coherent solution addressing all concerns regarding local
> variables.
>
>
>
> Thanks,
>
> Dana
>
>
>
> PS
>
> Can you remind me/us of the deadlines we should meet for this PAR.
>
>
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Tuesday, March 15, 2011 2:01 PM
> *To:* 'sv-ac@eda-stds.org'
> *Subject:* [sv-ac] Open Mantis items
>
>
>
> Hi all,
>
>
>
> I am attaching a spreadsheet with open Mantis items along with the
> recommendations regarding their processing made at SV-AC F2F meeting.
>
>
>
> The following recommendations have been made:
>
> · WIP – the items are targeted to be addressed at the current PAR
>
> · Postpone – the items are not targeted to be addressed at the
> current PAR (to be addressed or reevaluated at the next PAR)
>
> · Next PAR – items targeted for the current PAR, but we don’t have
> a sufficient bandwidth to address them now.
>
> · Close – the items are non-relevant or duplicate.
>
> · Address if feasible – the item owner to decide.
>
>
>
> Every item was assigned an owner.
>
>
>
> Action items required from the item owner:
>
> · Check whether you agree with the recommendation. If you don’t,
> send an email with an alternative recommendation to be discussed in the
> SV-AC meeting.
>
> · If the recommendation is “address if feasible”, modify it to WIP
> if you intend working on it during this PAR or to Postpone otherwise. If
> your recommendation is different from these two, send an email with a
> discussion request.
>
> · If the ultimate recommendation is “Close”, confirm this
> recommendation by email and we will vote to resolve this item as “No change
> required”.
>
> · Set the priority of issues ultimately marked as WIP and Close to
> high, to all other issues to low.
>
>
>
> Thanks,
>
> Dmitry
>
> ---------------------------------------------------------------------
> 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, and is
believed to be clean.