5 ms·
"SAT solvers became a billion-dollar industry" Does anyone have a reference for this?
by vok 6y ago
"SAT solvers became a billion-dollar industry"
Does anyone have a reference for this?
- yaantc 6y agoSAT is a key technology in electronic design automation (EDA), the industry making the tools allowing designing chips. From [1]: "Within EDA, SAT solvers are used for such disparate tasks as test pattern generation, circuit delay computation, logic optimization, combinational equivalence checking, bounded model checking and functional test vector generation." Improvement in SAT solving allows designing more and more complex chips. In software it's used for formal checking, through SMT (Satisfiability Modulo Theory [2]). SMT is an extension of SAT. For an example application, Microsoft is using their z3 SMT solver [3], now open source, for the automated Windows driver verification process. [1] https://semiengineering.com/knowledge_centers/eda-design/verification/sat-solver/ https://semiengineering.com/knowledge_centers/eda-design/ver... [2] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories [3] https://en.wikipedia.org/wiki/Z3_Theorem_Prover https://en.wikipedia.org/wiki/Z3_Theorem_Prover
- mhh__ 6y agoFDIV cost Intel hundreds of millions, formal verification is big money.