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.