Home > Community > Forums > Functional Verification > Formal Analysis Metrics

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: *

 Formal Analysis Metrics 

Last post Thu, Jan 26 2006 9:06 AM by archive. 1 replies.
Started by archive 26 Jan 2006 09:06 AM. Topic has 1 replies and 1280 views
Page 1 of 1 (2 items)
Sort Posts:
  • Thu, Jan 26 2006 9:06 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,950
    Formal Analysis Metrics Reply

    What kind of metrics are Formal Analysis users collecting?

    Below are some metrics I am or have thought about collecting for our designs.

    • The module that was verified
    • The version of the module that was verified and all associated files used in the run.
    • The HDL parameters that were used in the verification
    • The properties that were verified
    o Time it took for each property
    o Engines used for each property (time for each engine)
    o Explored Depth for properties not proved
    o Trigger: pass/fail, depth
    o Status: pass/fail depth
    • Percentage of state elements touched by proved properties

    Often times metrics are not kept and we lose track of what was verified, what is left to be verified, and how to best run the tool for future modules.


    Originally posted in cdnusers.org by ross.weber@unisys.com
    • Post Points: 0
  • Thu, Feb 2 2006 10:10 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,950
    RE: Formal Analysis Metrics Reply

    Hi,
    You almost left nothing for others :-) My 2 cents:

    I like to use Cover properties in a formal engine to look for tough corner cases that I couldn't hit in simulation. In that context here are few:

    * How many cover properties
    * How many got covered, can I write out HDL/HDVL tests from the formal tool for easy re-run/regress?
    * Integration of Formal + Coverage analysis (similar to what TransEDA seems to promote - not sure how much it works in reality).

    During our PSL book work, we explored few more interesting cases such as "latency analysis" etc. But tools were too immature then to handle a "battery of PSL code". Will be nice to get some recent experience on that front.

    Regards
    Ajeetha, CVC


    Originally posted in cdnusers.org by ajeetha
    • Post Points: 0
Page 1 of 1 (2 items)
Sort Posts:
Started by archive at 26 Jan 2006 09:06 AM. Topic has 1 replies.