Stats

  • Locked Locked
  • Replies 1
  • Subscribers 62
  • Views 13468
  • 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

The Value of SAT-Solvers in FV

archive

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 


Originally posted in cdnusers.org by djhulme
Parents

  • 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


    Originally posted in cdnusers.org by croy
Reply

  • 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


    Originally posted in cdnusers.org by croy
Children
No Data

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.