Home > Community > Forums > Functional Verification > Psl assertions for checking ECC

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 Psl assertions for checking ECC 

Last post Fri, Aug 17 2007 6:02 AM by archive. 9 replies.
Started by archive 17 Aug 2007 06:02 AM. Topic has 9 replies and 1910 views
Page 1 of 1 (10 items)
Sort Posts:
  • Fri, Aug 17 2007 6:02 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    Psl assertions for checking ECC Reply

    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,


    Originally posted in cdnusers.org by abna
    • Post Points: 0
  • Fri, Aug 17 2007 8:42 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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...


    Originally posted in cdnusers.org by stephenh
    • Post Points: 0
  • Mon, Aug 20 2007 10:14 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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.


    Originally posted in cdnusers.org by darrowchu
    • Post Points: 0
  • Mon, Aug 20 2007 10:20 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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.


    Originally posted in cdnusers.org by vincentr
    • Post Points: 0
  • Mon, Aug 20 2007 10:28 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    diagram attached....


    Originally posted in cdnusers.org by vincentr
    • Post Points: 0
  • Mon, Aug 20 2007 10:52 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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


    Originally posted in cdnusers.org by binju
    • Post Points: 0
  • Wed, Aug 22 2007 3:53 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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,


    Originally posted in cdnusers.org by abna
    • Post Points: 0
  • Wed, Aug 22 2007 4:08 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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.


    Originally posted in cdnusers.org by vincentr
    • Post Points: 0
  • Wed, Aug 22 2007 4:26 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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,


    Originally posted in cdnusers.org by abna
    • Post Points: 0
  • Fri, Sep 14 2007 12:10 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Psl assertions for checking ECC Reply

    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.


    Originally posted in cdnusers.org by darrowchu
    • Post Points: 0
Page 1 of 1 (10 items)
Sort Posts:
Started by archive at 17 Aug 2007 06:02 AM. Topic has 9 replies.