&quot;ATE (automatic test equipment)?&quot;<p>Yeah. It&#x27;s one of the only processes I have little data on. Must be straight-forward if I haven&#x27;t stumbled on many academic papers on the subject. If not, there&#x27;s a siloing effect happening on publishing side &amp; the term will be helpful.<p>&quot;The thing is that Intel does have the toughest job. They are 28nm with a complicated design, lots of RAM, power is a big issue so clock gating probably everywhere etc. You can&#x27;t really compare that with a military or an academic chip. The design constraints are much tougher for Intel.&quot;<p>That&#x27;s part of my point. Hitting perfection took making the problem a <i>lot</i> simpler than what Intel faced. Same happened in high assurance security where everything TCB was verified down to every trace and state. Took lots of geniuses...<p>&quot;Still, Intel supposedly has all the geniuses and the money. They should have no excuses.&quot;<p>...but still couldn&#x27;t solve all the problems, keep up in feature parity, meet profit requirements, etc. So, I&#x27;m not so harsh on Intel for now given the complexity &amp; business model. I might change my mind later. For now, we&#x27;ll just disagree. :)<p>&quot;On the formal stuff, I have yet to be convinced. I never just trust the tools, remember?&quot;<p>Now, that I don&#x27;t get. I&#x27;ve seen, in synthesis&#x2F;verification work, one 9-transistor analog circuit take (IIRC) 55,000+ equations to represent all its behaviors. Digital ones easier but with tons of multi-layer cells wired up. For custom, they often behave differently. DRC&#x27;s on modern nodes I read are in 1,000-2,500 range. I&#x27;m ignoring OPC because you&#x27;re handicapped enough at this point. If you don&#x27;t trust the tools, how are you getting anything done in ASIC land?<p>You must write really fast plus have a discount card at Office Depot to do it all on pencil and paper. :P<p>I think you trust tools more than you&#x27;re letting on. You probably just cross-check tools with tools in various ways like I did with high assurance SW to catch tool-specific issues. That implies a lot of, but not total, trust in the tools. If I&#x27;m wrong, I&#x27;ll be surprised and probably learn something in the process.<p>There&#x27;s another method HW people might already use that comes from theorem provers. They know the proving process is complex. It also breaks down into a series of primitive actions in logic. So, they split the activity between a complex, untrusted prover and a simple, easy-to-verify checker. I know state-machine equivalence &amp; even many physical phenomenon can be modeled well in software. I&#x27;ve seen as much with FEC systems. Trick for HW might be turning all the tool outputs into a series of steps like in an audit log that such tools can verify. That might take a <i>hell</i> of a long time, though, but also should be easy to parallelize onto clusters, GPU&#x27;s, FPGA&#x27;s, etc. Do it on a macro-cell at a time composing the results like in proof abstraction or abstract interpretation for software.<p>What you think?