Why chip companies care

In 1994 Intel shipped a Pentium with a faulty floating-point divider. The Pentium FDIV bug recall cost roughly $475 million in 1994 dollars — about $1.05 billion in 2026 USD after CPI adjustment — and is the textbook reason hardware verification matters. Today, before silicon goes to a fab, designers run equivalence checking: does this gate-level netlist compute the same function as the RTL spec? That question is encoded as a SAT instance — millions of clauses, hundreds of thousands of variables — and fed to industrial solvers descended from MiniSat: Glucose, CaDiCaL, Kissat. Cadence Conformal, Synopsys Formality, and OneSpin are SAT solvers wearing EDA suits. A modern mask set runs $5–30M (2026 USD) for typical nodes and well into nine figures at the leading edge; you want SAT to say UNSAT before you tape out.