PSL Assertion

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?

yes.

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 written

property 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%20verification

Look for "Session 1.8: Formal Analysis of Padring Mux-Logic Using IFV (Incisive Formal Verifier)"

Regards,
Joerg.