Psl assertions for checking ECC

I believe this has been done by several Cadence customers, with good success and some bugs found.
Rather than trying to implement the actual ECC calculations in PSL or SVA, I think some auxiliary HDL code was written so simplify the assertions.

I'll let one of my colleagues respond with some more detailed explanations...

Attached slide shows an example that you can verify your ECC generation/correction logic. The auxiliary RTL mentioned by Steve is just (data_i ^ error_bv). Hope it helps.

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.

diagram attached....

Hi:

Just want to add a couple more comments on this. I have done this with a couple customers. Hemming style ECC turns out to be a very good application for assertion with formal. For a 32 bits ecc, it can be done within minutes, and I have tried as big as around 250 bits ecc, and IFV managed to prove them.

Have fun with it.

Bin

Hi all,

For the ECC,I have just interested in the encoding part and I don't have the decoding part.
Have you an approch to verify this encoding part using the formal methodology?

Thanks,

hi,

Other than running a reference encoder in parallel and writing an assertion to say that both outputs must always be the same, I am not aware of another way to verify this with assertions.

I assume that there will be a decoder block somewhere in the larger system, or is the ECC data the final output of the chip?
If you could get the decoder then the previous method will verify both parts.

Regards,
Vince.

In fact, you have to verify only the ECC. In input you have data (16 bit or 8 bit) and in output you have the ECC is composed of ECC1(7 bit), ECC2(7bit) and ECC3(7 bit).
In attach,the file that describ the ECC(the encoding part).

Thanks,

Using formal methodology to verify ECC encoding part, I agree with Vince, you need to have a ECC encoder reference model, which is also synthesizable. Let the formal tool randomize your data inputs and use one assertion to check the ECC output. The assertion should say: design output and the reference model output should always be the same.