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> wrote:

> Yes, this is correct.
>
> Dmitry
>
> -----Original Message-----
> From: 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
> 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]
> > Sent: Monday, June 14, 2010 9:10 AM
> > To: Bresticker, Shalom
> > Cc: 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] On
> > >> Behalf Of Sayantan Das
> > >> Sent: Monday, June 14, 2010 8:51 AM
> > >> To: 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.
>
>
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.