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

Hi Dana,
 
For those of us, who are not familiar with PSL semantics, is there some
document to compare current SVA semantics with PSL semantics. Since
localvars in PSL were added after SVA localvars, what was the motivation
for keeping the semantics different from SVA ? Basically, I want to
understand what exactly is in PSL and how it compares to SVA.
 
Ben, based on your proposal, it looks like you expect tools to figure
out the ordering of read/write and give out errors at compile time. This
type of analysis may be time consuming and may add restrictions. Should
this really be tool's reponsibility. Or it should be part of user's
responsibility.
 
Manisha

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Dana
Fisman
Sent: Thursday, March 24, 2011 1:36 PM
To: Dana Fisman; ben@systemverilog.us; Dana Fisman
Cc: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: [sv-ac] RE: Open Mantis items

Hi Dmitry,

Note that this also explains how this issue is related to 3057. Item
3057 suggests we can declare a variable anywhere within a property or
sequence, and its scope is defined as the parenthesis encapsulating its
declaration. Once we have that, one should ask what is the difference
between

(logic v, ( .... v=expr1) intersect ( .... v=expr2) )

and

((logic v, .... v=expr1) intersect (logic v, .... v=expr2))

an answer that is consistent with how variables are defined in other
languages, e.g. C, is that v is the same variable in both operands of
intersect in the first example but a different, local, variable in the
both operands of the second example. This is not true in the current
approach of SVA since v is a different variable in both operands of the
first example. It is true in PSL.

Note, Ben, that we can get closer in terms of compatibility, if we adopt
the PSL semantics but allow declaring a variable of same name in both
operands (we can think of some preprocessing taking place that renames
the variables declared in the different operands to have different
names, e.g. l.v and r.v).

Dana

From: Dana Fisman [mailto:dfisman@synopsys.COM]
Sent: Thursday, March 24, 2011 9:49 AM
To: ben@systemverilog.us; Dana Fisman
Cc: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: [sv-ac] RE: Open Mantis items

Hi Ben,

Yes, there will be some backwards compatibility issues if we adopt the
PSL semantics. Indeed, in order to let a local variable have different
behavior in different branches of and/intersect you need to either
explicitly free it, or declare a different one in one of the threads. So
the cons are backwards compatibility issues but the pros are that the
semantics is simple and clear, intersect is intersect and not something
else, distributivity does not break, and no syntactic restrictions are
needed.

With regard to the examples below, they will pass in PSL since the RHS
of |-> is a tautology. Even if you change to an RHS which is not a
tautology they will pass since the LHS of |-> is a contradiction. The
LHS is a contradiction since v1 takes different values in the first
cycle of the operands of AND.

You can modify the LHS not to be a contradiction by declaring a
different variable in each of the operands:

  property P1_ala_PSL;

    (logic vl; ($rose(a), vl=0) ##1 b && !vl) and

    (logic vr; (c, vr=1) ##1 d && vr)) |-> ...

  endproperty

Dana

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Wednesday, March 23, 2011 11:24 PM
To: Dana Fisman
Cc: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: Re: [sv-ac] RE: Open Mantis items

Dana,

<Thus, if a local variable v appears in both branches of intersect it
should have the same value throughout in each of the cycles.>

Adopting the PSL approach is a compatibility issue to IEEE 1800-2009
because in SVA, the values of the local variables can take on different
values in each of the threads of the LHS and RHS of the and/intersect .
Below is a model that works OK in SVA.

I did not keep up with PSL, but if what you say above is true about PSL,
aP1 and aP2 assertions expressed in PSL would fail.

// In model below, property P1 and P2 both start at 30ns and
successfully pass at time 70ns.

module test4and;

  logic a=0, b=1, c=1, d=1, e=1, clk=0;

  initial forever #10 clk=!clk;

  initial begin

    @ (posedge clk) a <=1'b1;

  end

  property P1;

   logic v1, v2;

    (($rose(a), v1=0) ##1 b && !v1) and

    ((c, v1=1) ##1 d && v1) |=> 1;

  endproperty : P1

  aP1: assert property(@ (posedge clk) P1);

  property P2;

   logic v1, v2;

    (($rose(a), v1=0, v2=1) ##1 b && !v1) and

    // ((c, v1=1) ##1 d && v2) |=> 1; // illegal in IEEE 1800-2009

    ((c, v1=1, v2=0) ##1 d && !v2) |=> 1; // legal in IEEE 1800-2009

  endproperty : P2

  aP2: assert property(@ (posedge clk) P2);

endmodule : test4and

Ben Cohen SystemVerilog.us

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 freed 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 <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.