Hello Forum,
I am writing a SVA for following
There are 2 variables ‘a’ & ‘b’. After 3 clock cycles ‘b’ should have same value as ‘a’
My 1st attempt works fine
property p1;
int local_data;
@(posedge clk) ( 1 , local_data = a ) ##3 ( b == local_data ) ;
endproperty
ap1_test: assert property( p1 ) $display("Pass at time: %2t", $time );
else $error("Failure at time:%2t" , $time );
As an alternative I tried ::
property p2;
int local_data;
@(posedge clk) ( 1 , local_data = a ) |-> ##3 ( b == local_data ); // Why is consequent Legal ?
endproperty
ap2_test: assert property( p2 ) $display("Pass at time: %2t", $time );
else $error("Failure at time:%2t" , $time );
I am confused on the working of the consequent. As per LRM
Sequences can be composed by concatenation, analogous to a concatenation of lists.
The concatenation specifies a delay, using ##, from the end of the first sequence until the beginning of the second sequence
Since ‘##N’ is used between 2 sequence expressions, and the consequent has only 1 sequence expression i.e ( b == local_data ),
I believed that it should result in compilation error (although the code is legal when I simulated)
To make it legal one should add an always true sequence expression (1)
property p2;
int local_data;
@(posedge clk) ( 1 , local_data = a ) |-> 1 ##3 ( b == local_data ); // 1 is seqeunce expression
endproperty
ap2_test: assert property( p2 ) $display("Pass at time: %2t", $time );
else $error("Failure at time:%2t" , $time );
Why is the consequent ’ ##3 ( b == local_data ); ’ considered legal even though there is no sequence expression preceding ##3 ?