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

Thanks a lot to all of you

Regards

Sayantan

Bresticker, Shalom wrote:
> 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.