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 Assertion 

Last post Tue, Jul 10 2007 8:11 AM by archive. 5 replies.
Started by archive 10 Jul 2007 08:11 AM. Topic has 5 replies and 1750 views
Page 1 of 1 (6 items)
Sort Posts:
  • Tue, Jul 10 2007 8:11 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    PSL Assertion Reply

    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?


    Originally posted in cdnusers.org by vlsi_dude
    • Post Points: 0
  • Tue, Jul 10 2007 8:21 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL Assertion Reply

    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.


    Originally posted in cdnusers.org by jmueller
    • Post Points: 0
  • Wed, Jul 11 2007 1:45 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL Assertion Reply

    Thanks Joerg.

    Can we synthesize these PSL assertion?


    Originally posted in cdnusers.org by vlsi_dude
    • Post Points: 0
  • Wed, Jul 11 2007 1:47 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL Assertion Reply

    yes.


    Originally posted in cdnusers.org by jmueller
    • Post Points: 0
  • Wed, Jul 11 2007 6:35 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL Assertion Reply

    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


    Originally posted in cdnusers.org by vlsi_dude
    • Post Points: 0
  • Thu, Jul 12 2007 2:12 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL Assertion Reply

    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.


    Originally posted in cdnusers.org by jmueller
    • Post Points: 0
Page 1 of 1 (6 items)
Sort Posts:
Started by archive at 10 Jul 2007 08:11 AM. Topic has 5 replies.