Comment by screcth | Hacker News Reader

Comment by screcth | Hacker News Reader

Parent Full thread

Formal hardware verification has been much more successful in industry. Are there fundamental differences in the types of problems that they solve? EDA companies have been able to create tools that don't require a PhD in Math to be used effectively.

I think that the explanation for such different levels of success is that economic incentives are different. The cost of a hardware bug is much much higher than the cost of the average software bug; this means that hardware companies are willing to spend a lot of money in getting designs right the first time, versus software companies that know they can always make bug fixes in new versions of their products. Additionally, hardware companies are used to paying millions of dollars in software licenses, which is not common in the software world.

Yeah I agree formal hardware verification is an order of magnitude easier to use.

My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc.

Yes, the challenge in any formal software verification is dealing with unbounded inputs and compute durations, as enabled by recursive programs. If the code under analysis is straight-line non-reentrant basic logical blocks, the verification is quite trivial indeed. This is vaguely the case for hardware verification, though of course there are complexities introduced by the physical nature of the embedding.

> My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc.

My guess: it's because people actually care about correctness for hardware. It's really expensive to throw out all those fab runs when you notice you messed up...

That would only cover the simplest feed-forward designs: combinational circuits and versions with extra registers added for timing reasons.

As soon as you introduce any kind of feedback in your RTL design it's possible to do any kind of computation that SW can do and therefore proving correctness is difficult.

Reply on news.ycombinator.com