Is it useful to write the psl assertions for checking the CRC?
How I can write the PSL assertion for interface signal between two modules? Any Example?
Hey Dude,1) CRC checking can be done by creating 2 signals: A the original vector with CRC field. B the same vector with one bit flipped (this is a constraint like "countones(A xor B) = 1"). The vector itself is unconstrained, but the CRC field needs to be correctly calculated. Your CRC decoder should provide the corrected vector on the output. Similary you can detect 2 flipped bits. IFV did pretty good jobs with CRC blocks in the past.2) pure connectivity checking is described in a paper from Freescale at CDNLive 2006 Silicon Valley. Please browse the proceedings there.Joerg.
Thanks Joerg.Can we synthesize these PSL assertion?
I am writing psl assertion for interfacing signals from one module to another module.Like if Module A has signal sigA1 which is connected to Module B of signal sigB1, then i have writtenproperty prop1 = always (A.sigA1 == B.sigB1)@(posedge CLK);assert prop1;Whether this is the correct way to write for interface signal or any other method we can use?Also Whether this type of assertions are useful?Thanks
Hi Dude,this is a correct assertion to verify connectivity between 2 arbitrary points in your design. You may need to remove the other drivers of sigA1 to improve performance. More information on that type of verification can be found at http://www.cdnusers.org/CDNLive/SiliconValley2006Proceedings/tabid/366/Default.aspx?topic=Functional%20verificationLook for "Session 1.8: Formal Analysis of Padring Mux-Logic Using IFV (Incisive Formal Verifier)"Regards,Joerg.