Stats

  • Locked Locked
  • Replies 3
  • Subscribers 61
  • Views 17931
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

Conformal struggles to resolve abort points (due to complex logic)

archive

Conformal (XL) version: v7.2-p100
Equivalent checking purpose: RTL vs Netlist
Synthesis Tool : Synopsys Design Compiler

Formality passes & Conformal struggling & left 17 abort points. 

Conformal vs Formality

From the 4000-something compare points in the design Conformal rather quickly down to 40 remaining

compare points then gave up. Addition of extra effort options brought it down from 40 to 17 remaining

compare points, Conformal gave up again.

On the other hand, Formality (Synopsys) only needs 1-1.5hrs to finish formal verification. You may argue that Formality & DC shares the same VHDL parser and thus they have better understanding with each others!



I did run "analyze abort -compare" (as what always Conformal suggests..) at the point where Conformal stucks at 40 abort points, consequence of running this command will then bring the number of aborting points to 17.

Conformal version 7.2-p100 will automatically executing the following actions when executing "analyze abort -compare":-

(note from administrator - portions of this post have been deleted as sensitive material, with permission of the author)
Anyhow, this doesn't give any benefit on bringing these 17 abort points at all.

The following are the log files of the run:-
(administrator note: portions of this log file have been deleted with permission of the original poster - as sensitive information)
// Warning: Key point mapping is incomplete
// Note: mult_75: failed to find boundary
// Note: mult_75: quality evaluated 85% success
// Note: add_418_0(clustered): quality evaluated 100% success
// Running automatic setup...                                                           
// Remodeling sequential constants...
// Remodeling Golden ...
// Identified 1 DFF/DLAT(s) as sequential constant in (G).
// Remodeling Revised ...
// Converted 1 DFF/DLAT(s) in (G) to ZERO/ONE
// Automatic setup finished.
// 4567 compared points added to compare list
================================================================================
Compared points      PO     DFF    DLAT   BBOX      Total  
--------------------------------------------------------------------------------
Equivalent           368    4145   1      12        4526   
--------------------------------------------------------------------------------
Inverted-equivalent  0      1      0      0         1      
--------------------------------------------------------------------------------
Abort                0      40     0      0         40     
================================================================================
LEC> analyze abort -compare
================================================================================
Compared points      PO     DFF    DLAT   BBOX      Total  
--------------------------------------------------------------------------------
Equivalent           368    4168   1      12        4549   
--------------------------------------------------------------------------------
Inverted-equivalent  0      1      0      0         1      
--------------------------------------------------------------------------------
Abort                0      17     0      0         17     
================================================================================

I suspect that the root cause of this due to Conformal not be able to evaluate some of the complex multiplexers and adders.

"// Note: mult_75: failed to find boundary
// Note: mult_75: quality evaluated 85% success
// Note: add_418_0(clustered): quality evaluated 100% success"

Any suggestion to move this forward will be highly appriciated.

Thanks.


Originally posted in cdnusers.org by cheksan
abort_7.2p100.log.gz

  • Hi cheksan

    Yes, the 'failed to find boundary' message is pobably the root cause of the problem here. I'm quite surprised that 'analyze abort -compare' helped so little.

    Please file a service request (SR) so we can help.

    Chrystian


    Originally posted in cdnusers.org by croy

  • Hi Chrystian,

    Problem can be solved if taking the following approach:-

    set flatten model -gated_block

    # Don't analyze any abort points
    set analyze option -nonanalyze_abort

    # Modeling & setup
    set system lec

    # analyze datapath after modeling & setup
    Analyze -datapath -versbose

    The result of this flow is that the first multiplexer has been evaluated 85% compare to fails (0%) before.

    "// Note: mult_75: quality evaluated 85% success
    // Note: mult_75: quality evaluated 85% success
    // Note: add_418_0(clustered): quality evaluated 100% success"

    Hope this is useful ;-)

    Regards,
    Chek San


    Originally posted in cdnusers.org by cheksan

  • Hmm . . . Interesting!
    One series of commands leads to aborts but the other leads to clean run.

    Cheksan, please file an SR as Chrystian suggested. We consider these very serious and will try to address this with our R&D teams. Curiously, how was your run time with the second cleaner flow?

    Thanks!
    - mm


    Originally posted in cdnusers.org by makkarm

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.