Psl assertions for checking ECC > Forums

Unanswered

Active Topics

Forums

Forums > Functional Verification > Assertion-Based Verification and Formal Analysis

Subject: Psl assertions for checking ECC

Posting to forums is available to community members only.
Login or Register

Rate this topic:

Author

Messages

abna
Posts: 6
Online: User is Offline

8/17/2007 6:02 AM
Hi all, I would like to know if it useful to write the psl assertions for checking the ECC(error correction code).The ECC is a standard algorithm(Hamming Code). Thanks,

stephenh
Posts: 77
Online: User is Offline

8/17/2007 8:42 AM
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...

Steve H.

darrowchu
Posts: 4
Online: User is Offline

8/20/2007 10:14 AM
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.
Attachment: ECC_assertion.pdf

vincentr
Posts: 6
Online: User is Offline

8/20/2007 10:20 AM
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.

vincentr
Posts: 6
Online: User is Offline

8/20/2007 10:28 AM
diagram attached....

binju
Posts: 3
Online: User is Offline

8/20/2007 10:52 AM
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

abna
Posts: 6
Online: User is Offline

8/22/2007 3:53 AM
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,

vincentr
Posts: 6
Online: User is Offline

8/22/2007 4:08 AM
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.

abna
Posts: 6
Online: User is Offline

8/22/2007 4:26 AM
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,
Attachment: ECC_ifv.zip

darrowchu
Posts: 4
Online: User is Offline

9/14/2007 12:10 AM
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.

Posting to forums is available to community members only.
Login or Register

Forums > Functional Verification > Assertion-Based Verification and Formal Analysis > Psl assertions for checking ECC

ActiveForums 3.6