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