SAT-Solvers in Formal Verification

Hello,

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

I am looking for an application for them and I’ve been told that SAT-Solvers are used throughout the Formal Verification process in the EDA industry, and 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.

Kind regards,

Daniel

djhulme said:

Hello,

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

I am looking for an application for them and I’ve been told that SAT-Solvers are used throughout the Formal Verification process in the EDA industry, and 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.

Kind regards,

Daniel

Click to expand...

Here are a couple links to get you reading...

http://www.satlive.org/
http://research.microsoft.com/users/lintaoz/papers/dac_2001.pdf
http://www.cs.sfu.ca/~mitchell/papers/colLogCS85.pdf
http://www.satlib.org/solvers.html

...Don't forget to press the Helped Me buton...

Thank you for these. I'm very familiar with the technology, it's information about where SAT sits in the FV process that I need.

Also, in essense I'd like to know the commercial potential of a SAT solver that can perform better than current state-of-the-art.

How do you convert a FV test problem into SAT? (from a FV perspective - i know about De Morgans law, etc)
What types of test problems are converted into SAT? (in laymans)
How many problems are ran on SAT-Solvers per month for a given chip?
What percentage of the EDA/FV process is taken up using SAT?
What are the time and costs involved in the use of SAT solvers in FV?
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