RE: [sv-ac] Semantics of indexed expression in assertion.

Yes, in general, x is considered false.

2'b0x reduces to x because if the x is 0, the result is false, and if the x is 1, the result is true.

2'b1x is true because it is always different from 0.

Shalom

________________________________
From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Monday, June 14, 2010 9:50 AM
To: Korchemny, Dmitry
Cc: Bresticker, Shalom; Sayantan Das; sv-ac@eda.org
Subject: Re: [sv-ac] Semantics of indexed expression in assertion.

Changed the model since bit cannot be X.
 logic b=0;
  assign a= 2'b1x;
  always begin #1
    if(a) b=1;
   end
A simulation shows that at time 1, b goes from 0 to 1. Thus, 2'b1x is considered "true"
  However, changing the code to "assign a= 2'b0x;: yielded a simulation with a=0 at all times.
Thus, 2'b1x is true
          2'b0x is false
Thus, true is anything greater than 0, else it is false.

Code:
module vector_in_assertion(CLK, ACK);
  input CLK;
  input ACK;
  logic [1:0] a;
  logic b=0;
  assign a= 2'b0x;
  always begin #1
    if(a) b=1;
   end

// VEC_IN_CONCAT : assert property(@(posedge CLK) ACK |=> (a[1:0] ##1 ACK ) );

// VEC_NO_CONCAT : assert property(@(posedge CLK) ACK |=> a[1:0] );
// VEC_NO_CONCAT_WITH_PAST : assert property(@(posedge CLK) ACK |=> $past (a[1:0]) );
endmodule
Ben

On Sun, Jun 13, 2010 at 11:36 PM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
Yes, this is correct.

Dmitry

-----Original Message-----
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 Bresticker, Shalom
Sent: Monday, June 14, 2010 9:13 AM
To: Sayantan Das
Cc: sv-ac@eda.org<mailto:sv-ac@eda.org>
Subject: RE: [sv-ac] Semantics of indexed expression in assertion.

Unless the result is unknown, such as 2'b0x.

Unless SV-AC experts tell us that assertions work differently.

Shalom

> -----Original Message-----
> From: Sayantan Das [mailto:sayantan@verific.com<mailto:sayantan@verific.com>]
> Sent: Monday, June 14, 2010 9:10 AM
> To: Bresticker, Shalom
> Cc: sv-ac@eda.org<mailto:sv-ac@eda.org>
> Subject: Re: [sv-ac] Semantics of indexed expression in assertion.
>
> Hi Shalom,
>
> Thanks for the reply.
>
> Just to clarify if a[1:0] equal to 2'b00 then the expression a[1:0]
> should return false and any other value should true.
>
> Or in other words we should consider disjunction of the bits.
>
> Please correct me if I am wrong
>
> Thanks
> Sayantan
>
> Bresticker, Shalom wrote:
> > General SV semantics would dictate that TRUE == "different
> from zero" and FALSE == "zero".
> >
> > Shalom
> >
> >
> >> -----Original Message-----
> >> 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 Sayantan Das
> >> Sent: Monday, June 14, 2010 8:51 AM
> >> To: sv-ac@eda.org<mailto:sv-ac@eda.org>
> >> Subject: [sv-ac] Semantics of indexed expression in assertion.
> >>
> >> Hi ,
> >>
> >> I have the following query.
> >>
> >> Please look at the design below.
> >>
> >> /
> >> module vector_in_assertion(CLK, ACK);
> >> input CLK;
> >> input ACK;
> >> bit [1:0] a;
> >>
> >>
> >> VEC_IN_CONCAT : assert property(@(posedge CLK) ACK |=>
> >> (a[1:0] ##1
> >> ACK ) );
> >>
> >> VEC_NO_CONCAT : assert property(@(posedge CLK) ACK |=>
> a[1:0] );
> >>
> >> VEC_NO_CONCAT_WITH_PAST : assert property(@(posedge
> CLK) ACK |=>
> >> $past (a[1:0]) );
> >> endmodule
> >>
> >>
> >> /Here I am confused with the semantics of the assertions
> >> (i.e. when they
> >> should pass and when should they fail)
> >>
> >> Foe example, In /VEC_IN_CONCAT /How should the LHS of the Concat
> >> operator should be evaluated. Given a[1:0] should we only
> look at the
> >> LSB(or MSB) or the disjunction of the bits.
> >>
> >> Moreover is the semantics similar if used elsewhere like in
> >> /VEC_NO_CONCAT and //VEC_NO_CONCAT_WITH_PAST.
> >>
> >> /Thanks in advance
> >>
> >> Regards
> >> Sayantan
> >>
> >> --
> >> This message has been scanned for viruses and
> >> dangerous content by MailScanner, 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.
> >
> >
> >
>
>
---------------------------------------------------------------------
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, 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, 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, and is
believed to be clean.