That's true, but may be changing.
> a) the state space is much smaller than for software (although it can still be prohibitively large for complex designs and brute force formal methods)
That's true as well, but that is why some formal methods -- like my favorite, TLA+, and all the sound static analysis tools (they work by abstract interpretation) -- try to tackle the problem of software verification by abstraction (in a precise mathematical sense, namely a description of the system using a sound approximation of one with fewer states). In TLA+ you can even describe your system in different levels of detail and show that they form a sound abstraction/refinement relation. This is not to say that it's a silver bullet -- it takes work and thought, and isn't appropriate for everything, but a system like TLA+ lets you at least choose the level of detail you wish to work in and so the cost you'll have to pay. The lower the level, the more confidence you get, but more work you need to do. The early signs of TLA+'s success in industry show the practice to be worthwhile in some/many very important -- and quite common -- circumstances.
True, "trial runs" for asic production cost impossibly huge amounts of money as mask sets cost so much to make even for a 3 generations old process.
Only top players can afford them, yet some of them do switch do limit themselves to extensive verification.
Another big thing is time, doing a trial run in actual silicon takes many times more time than the most extensive verification run you can afford for an equivalent amount of money on current mainstream litho process.
There are only few software products that are formally verified. Some data diodes and real time operating systems (at least partially).
That depends what you mean by "formally verified". If you mean verification all the way from global, high-level properties and down to program code or even machine code -- what's known as end-to-end verification -- and that the verification method is deductive proof, then you're right. But there is plenty of embedded software that's verified end-to-end with model checkers, and a growing list of popular software that's verified by various means, but not end-to-end, for example most of Amazon's web services.
For everything else, people use the good old functional verification because more the state complexity of more complex designs simply explodes.