Accellera SuperVerilog Assertion Activity: RE: [sv-ac] RE: Open

From: Dana Fisman <Dana.Fisman@synopsys.com>
Date: Mon Mar 21 2011 - 01:44:20 PDT

Ooops, accidentally pressed "send"... Here is the entire email.

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 that if we do so then there is no need to (a) specify the variables are automatic (i.e. remain the same throughout) and (b) impose the order restrictions that you propose. Since there are not really reads and writes taking place. The examples you give as illegal will work just fine. Take for instance the your first illegal example. Wasn't sure about precedence, so let's look at both options.

property P_cycle_v1;
automatic int v,w;
((w, v=data) ##[1:3] a and (v, w=addr) ##1 f) implies (c==v ##2 d)
endproperty :P_cycle

Since each local variable (i.e. both v and w) is assigned only once, the value will remain stable throughout and so there is no need for the "automatic" qualification. Regarding the order, for the formula to fail or pass non-vacuously, the LHS of implies must hold, and so both the LHS and RHS of and should hold. Suppose we evaluate the formula at time k then for the RHS of and to hold, v should hold at cycle k and w should obtain the value of addr on cycle k, for the LHS of and to hold, w should hold at cycle k and v should obtain the value of data at cycle k. Then if a and f occur when expected , the value of c at cycle k should be that of v which is data at cycle k.

property P_cycle_v2;
automatic int v,w;
(w, v=data) ##[1:3] a and ((v, w=addr) ##1 f implies (c==v ##2 d))
endproperty :P_cycle

For the property to hold both LHS and RHS of and should hold. If we evaluate at cycle k, for LHS to hold, w should hold v should take the value of data at cycle k. For rhs to hold, either LHS of implies fails or both LHS and RHS of implies hold. If v holds in cycle k, then w will take the value of addr at cycle k, and if f holds when expected, then c should equal the value of v i.e. of data at cycle k. If v does not hold on cycle k, there is no requirement imposed on c.

Note also that if we have something like ((a, v=data1) intersect (b, v=data2)) that is fine too. If data1 is different from data2 then this expression equals false, otherwise it equals a && b.

Thus, I don't see why we need the order restrictions. Am I missing something?

Thanks,
Dana

Hi Ben,

Now let's interpret the examples in your proposal as in PSL. It seems to me t

From: ben cohen [mailto:hdlcohen@gmail.com]<mailto:[mailto:hdlcohen@gmail.com]>
Sent: Thursday, March 17, 2011 5:28 PM
To: Korchemny, Dmitry
Cc: Dana Fisman; sv-ac@eda-stds.org<mailto: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<mailto: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<mailto:Dana.Fisman@synopsys.com>]
Sent: Wednesday, March 16, 2011 09:03
To: Korchemny, Dmitry; 'sv-ac@eda-stds.org<mailto: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> [mailto: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<mailto: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.

Received on Mon Mar 21 01:45:06 2011

This archive was generated by hypermail 2.1.8 : Mon Mar 21 2011 - 01:45:11 PDT

RE: [sv-ac] RE: Open Mantis items