> 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...
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.
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.
My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc.