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.