&quot;That&#x27;s why I am not a fan of formal methods. Nothing is proven until you have it working in silicon.&quot;<p>The one&#x27;s that did use formal methods all the way did what they were supposed to and usually first pass. They were a mix of academic and defense-related stuff most people can&#x27;t buy. What I normally see when I look up formal verification in industry is equivalence checking with custom shops also doing protocol verification and certain correctness angles. We&#x27;ve seen lots of what Intel does in their docs. So, that narrows the question down to &quot;Why are these errata in there anyway?&quot;<p>&quot;The big 3 of EDA tools (Cadence, Synopsis, Mentor Graphics) provide their own tools for verifying this stuff called UVM. Like anything, it still relies on the person using the tool. It takes a lot of effort and planning to use this stuff.&quot;<p>Didn&#x27;t know about that one. Thanks. The briefs I just Googled sound weaker than Intel&#x27;s stuff and especially IBM&#x27;s where presentations cover an incredible amount of specific verifications. Like you said, what one puts in determines what one gets out of it. So, are Intel just being lax on verification or is their stuff just too complex + optimized to catch all the corner cases?<p>&quot;Intel has a rep for letting bugs go to silicon despite all that stuff. &quot;<p><i>If</i> it&#x27;s intentional and avoidable, then I think it might be wise in another light. (Or not, but worth considering.) The other light is the Lipner essay on why shipping is more important than highest quality:<p><a href="https:&#x2F;&#x2F;blogs.microsoft.com&#x2F;cybertrust&#x2F;2007&#x2F;08&#x2F;23&#x2F;the-ethics-of-perfection&#x2F;" rel="nofollow">https:&#x2F;&#x2F;blogs.microsoft.com&#x2F;cybertrust&#x2F;2007&#x2F;08&#x2F;23&#x2F;the-ethics...</a><p>That comes from a background where he and Karger did high assurance systems that aimed for perfection and got as close as they could in that period. Kept slipping behind competition in terms of features&#x2F;speed&#x2F;price and that would effect market share. So, his prior employer canceled that product with his next one following his recommendation to hit acceptable quality levels, ship, and continuosly improve the product. Wonder if Intel is doing that to keep market dominance?<p>&quot;Nothing is proven until you have it working in silicon.&quot;<p>This we agree on. The formally verified stuff usually works first try but that&#x27;s thanks to billions in R&amp;D in tooling &amp; fabs they used. I like knowing a batch of chips performed exactly according to spec when probed during operation. Funny I can&#x27;t remember what you HW people call that activity.<p>Anyway, I&#x27;d love to email or chat with you sometime to see an insider&#x27;s view on this topic and fill in some blanks. Reason being experienced ASIC people talk very little vs software people. I&#x27;m collecting what tidbits of reality I can for a variety of reasons. Two important ones are giving a head start to people aiming for HW design and boosting high assurance design by determining where the weak points are currently. Really busy right now but maybe later on, eh?