Wednesday, December 03, 2008     Register | Login | Search | Contact Us
     
   
     
     

Many of you already received communications about the move of the Cadence user community into cadence.com. And many of you have already joined, with over 4000 registrations in the first two weeks.

The new Cadence Community enhances the ability of Cadence users to connect and collaborate. In addition to moving the community into cadence.com -- enabling single sign-on for community, Sourcelink and Cadence events -- the new site is organized around nine technology segments, giving you easy access to product information, training, forums and blogs. Some of the new features include:
  • Ability to respond to posts via e-mail
  • Technology-specific blogs
  • Latest Web 2.0 social networking capabilities
  • Public profile options
  • Private messaging
  • Friends lists
Visit the new Cadence Community today at www.cadence.com/community and join the discussions!

Registration note: Due to the scope of the enhancements and the new SSO registration system, we were not able to migrate existing cdnusers.org member accounts. So new registrations are required, but this enables a broader set of functionality we think you'll enjoy.

Forum note: Under the guidance of forum moderators, we have taken the 20+ cdnusers.org forums and consolidated them into 11 forums on the new site. Posts have been brought over so you can leverage that posting history. CDNusers forums will be set to read only starting 7/30, and cdnusers.org will be redirected to the new community on 8/4.

Best regards,
Mike and Tom

Michael A. Catrambone - Steering Committee Chairman
Distinguished Engineer
PCB/Mechanical
UTStarcom, Inc.

Tom Diederich
Cadence Community Manager
Home
Forums
Forums > Digital IC > Formal verification

Subject: Conformal struggles to resolve abort points (due to complex logic)
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
cheksan
Posts: 2
Online: User is Offline
1/31/2008 7:58 AM  
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.

Attachment: abort_7.2p100.log.gz
croy
Posts: 54
Online: User is Offline
2/01/2008 5:52 AM  
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
cheksan
Posts: 2
Online: User is Offline
2/05/2008 2:43 AM  
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
makkarm
Posts: 9
Online: User is Offline
2/09/2008 7:51 PM  
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
Posting to forums is available to community members only.
Login or Register
Forums > Digital IC > Formal verification > Conformal struggles to resolve abort points (due to complex logic)


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.