Thursday, November 20, 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: The Value of SAT-Solvers in FV
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
djhulme
Posts: 1
Online: User is Offline
5/25/2007 9:07 AM  

Hello,

 

I am a researcher in University College London and I develop Boolean satisfiability algorithms (SAT-Solvers).

 

I am looking for an application for my algorithms, and I’ve been told that SAT-Solvers are used throughout the Formal Verification process in the EDA industry, and I would like to know more about it.

 

Could anyone tell me more about how SAT is applied to the FV process. Who uses it? Why is it used? How is it used? How much is it used? Names and numbers would be very helpful.

 

More specifically, in essence I'd like to know the commercial potential of a SAT-Solver that can perform better than current state-of-the-art in the FV industry.

 

1. How do you convert a FV test problem into SAT? (from a FV perspective – I’m very familiar with De Morgan’s law, etc)

2. What types of test problems are converted into SAT? (in layman’s)

3. How many problems are ran on SAT-Solvers per month for a given chip?

4. What percentage of the EDA/FV process is taken up using SAT?

5. What are the time and costs involved in the use of SAT solvers in FV?

6. How much benefit would a new SAT-Solver give to the FV process? Given that they are 10% 'faster' than other solvers, for instance.

 

Regards,

 

Daniel 

croy
Posts: 54
Online: User is Offline
6/01/2007 5:14 PM  
Cadence formal tools (including IFV and Conformal EC/CCD/CLP/Verify) use a variety of solvers. The actual details are a closely guarded secret for competitive reasons.

A Conformal user can influence the formal engine using 'set compare effort' (EC) or 'set prove effort' (CCD/Verify). The default is low (and that default gives the best performance across most designs). It can be bumped up to medium, high, or super. What those effort levels actually relate to, in terms of changes to the solvers called, I don't know. It's not something that's shared, even internally.

I'm sorry I can't really help.

Chrystian
Posting to forums is available to community members only.
Login or Register
Forums > Digital IC > Formal verification > The Value of SAT-Solvers in FV


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.