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