Evaluation at posedge of SVA assertions

92 views Asked by At

I am trying to write a simple assertion in systemverilog like the following :

 //Generate signal high during time where signals shouldn't change
 always @(posedge FCLK) begin
 if(cmd_typeA) begin
     verif_sig_Stable <= 1;
 end
 else if(cmd_typeB) begin
     verif_sig_Stable <= 0;
 end
 //else save the status
 end

//Assertion
Test_stability : assert property (
 @(verif_sig_Stable )
 verif_sig_Stable |-> $stable(Ready_sig)
 );

I want that during the duration that the flag is high, the Ready_sigstays at the same value. It seems to work quite well, except for positives edges of the verif flag, if my Ready_sig is also changnig. I have the case where Ready_sig changes at the exact same time step as the verif flag (positive edge), and the assertion is failed.

My understanding of the issue : The assertion is evaluated eveyr time the verif flag toggles (positive or negative edge), in case of positive edge, the evaluated value of the flag is zero, so the assertion is not checked since the LHS of the arrow is not true. In case of negative edge, the evaluated value of the verif flag is one, so the LHS is true, and at the same evaluation cycle, the value of Ready_sig has to be the same as the previous evaluation cycle. Which triggers as FAIL because it is not, since it changed just after the evaluation of assertion (but still in the same delta cycle).

I understood that the problem happens because at the evaluation event, the values evaluated are the ones just at the beginning of the time step, if they are changing at that moment. Since the RTL is triggered on the same time step and changes the values (combinatory path with mux), the behavior appears to be fine, but wrongly evaluated as error. This is creating a structural conflict between my RTL & the SVA evaluation because it will create an error every time.

I also tried to look at the events region of SystemVerilog, this question answer part of my issue : Unexpected SVA assertion behavior for a periodic signal

Do you know how to take the positive edge into account as PASS if Ready_sig is changing at the same time ?

0

There are 0 answers