Psl assertions for checking ECC

Hi,

I have performed ECC verification in the past using IFV and seen very good results. I'm attaching a diagram to help explain the approach I used - it assumes that your ECC block is made up of 2 parts; an encoding part and a decoding and correction part.

If you have both sides of the ECC flow then for formal verification they can be considered as 2 unconnected paths (structurally).

We can use assertions to bridge the 2 parts of the design as follows:

Please note, this explanation assumes that the design in combinatorial i.e. no register stages, and that at most a one-bit error can be corrected. I will expand on this after the basic explanation.


Encode:
The data presented to the Data_in port will have an ECC code generated for it and both the original Data_in and ECC code will then be presented on the DataECC_out port.

Decode:
Data and an ECC code is received on the DataECC_in port.
If there is at most a 1-bit error then the design will correct it and present the corrected data on the Data_out port.


Given this information the following high level behaviour can be written:

When there is at most 1 error between DataECC_out and DataECC_in then Data_out must be the same as Data_in.

In PSL this could be written as follows:


// Check that at most 1 corrupted bit will be corrected:
// psl output_Data_out : assert always
// ( (onehot0( DataECC_out ^ DataECC_in)) -> (Data_out == Data_in));


XOR-ing DataECC_out and DataECC_in will result in a 1 for every corresponding bit that is different between the 2 vectors.

The onehot0 function resturns TRUE when there are zero or one 1's in the vector passed to it.

Therefore the assertion only triggers when the decoder is expected to either maintain or correct the incoming data.


--------


If the correction unit can handle more than one error then you could use the "countones" function instead of onehot0.

e.g.

// Check that as many as 3 corrupted bits will be corrected:
// psl output_Data_out : assert always
// ( (countones( DataECC_out ^ DataECC_in) < 4) -> (Data_out == Data_in));


Both these assertions state that once the triggering condition has been met then the expected result will be true in the same cycle i.e. there are no register delays in the design.

For a design with register delays you will need to model the delay path in the assertion to match.

e.g.

// Check that as many as 3 corrupted bits will be corrected.
// There is a reg delay of 5 cycles through the decode unit.
// psl output_Data_out : assert always
// ( {countones( DataECC_out ^ DataECC_in) < 4} |-> {[*5]; (Data_out == prev(DataECC_out[[i]data_range[/i]],5))}) @(posedge clk);


To reduce state space for this assertion the 'golden' data has been referenced from the output of the encoder block, thus you do not need to include the delay through the encoder in this assertion.

However, this is not fully testing the design as in the previous examples as it could be possible that an error is introduced in the encoder block stage.

To fully verify the design and remain efficient a 2nd assertion is needed to check the path through the encoder stage:

// Check that data is not corrupted through the encoder.
// There is a reg delay of 7 cycles through the encoder unit.
// psl output_encoder_Data_out : assert always
// ( {[*7]; (DataECC_out[[i]data_range[/i]] == prev(Data_in,7))}) @(posedge clk);


Hope this was useful!

Vince.

Hi,

I have performed ECC verification in the past using IFV and seen very good results. I'm attaching a diagram to help explain the approach I used - it assumes that your ECC block is made up of 2 parts; an encoding part and a decoding and correction part.

If you have both sides of the ECC flow then for formal verification they can be considered as 2 unconnected paths (structurally).

We can use assertions to bridge the 2 parts of the design as follows:

Please note, this explanation assumes that the design in combinatorial i.e. no register stages, and that at most a one-bit error can be corrected. I will expand on this after the basic explanation.


Encode:
The data presented to the Data_in port will have an ECC code generated for it and both the original Data_in and ECC code will then be presented on the DataECC_out port.

Decode:
Data and an ECC code is received on the DataECC_in port.
If there is at most a 1-bit error then the design will correct it and present the corrected data on the Data_out port.


Given this information the following high level behaviour can be written:

When there is at most 1 error between DataECC_out and DataECC_in then Data_out must be the same as Data_in.

In PSL this could be written as follows:


// Check that at most 1 corrupted bit will be corrected:
// psl output_Data_out : assert always
// ( (onehot0( DataECC_out ^ DataECC_in)) -> (Data_out == Data_in));


XOR-ing DataECC_out and DataECC_in will result in a 1 for every corresponding bit that is different between the 2 vectors.

The onehot0 function resturns TRUE when there are zero or one 1's in the vector passed to it.

Therefore the assertion only triggers when the decoder is expected to either maintain or correct the incoming data.


--------


If the correction unit can handle more than one error then you could use the "countones" function instead of onehot0.

e.g.

// Check that as many as 3 corrupted bits will be corrected:
// psl output_Data_out : assert always
// ( (countones( DataECC_out ^ DataECC_in) < 4) -> (Data_out == Data_in));


Both these assertions state that once the triggering condition has been met then the expected result will be true in the same cycle i.e. there are no register delays in the design.

For a design with register delays you will need to model the delay path in the assertion to match.

e.g.

// Check that as many as 3 corrupted bits will be corrected.
// There is a reg delay of 5 cycles through the decode unit.
// psl output_Data_out : assert always
// ( {countones( DataECC_out ^ DataECC_in) < 4} |-> {[*5]; (Data_out == prev(DataECC_out[[i]data_range[/i]],5))}) @(posedge clk);


To reduce state space for this assertion the 'golden' data has been referenced from the output of the encoder block, thus you do not need to include the delay through the encoder in this assertion.

However, this is not fully testing the design as in the previous examples as it could be possible that an error is introduced in the encoder block stage.

To fully verify the design and remain efficient a 2nd assertion is needed to check the path through the encoder stage:

// Check that data is not corrupted through the encoder.
// There is a reg delay of 7 cycles through the encoder unit.
// psl output_encoder_Data_out : assert always
// ( {[*7]; (DataECC_out[[i]data_range[/i]] == prev(Data_in,7))}) @(posedge clk);


Hope this was useful!

Vince.