3 ms·

It's amazing how pretty much all HW development does formal verification business as usual.

• rkangel 10y ago
  Much smaller state space so a much easier problem than formally verifying software.
• pjc50 10y ago
  It's because you can't update hardware, and the NRE is huge. If every deploy cost you $250k you'd want formal verification too. Mostly the existing toolchain does formal equivalence checking, which isn't quite the same thing; it verifies that the behaviour of the output circuit is the same as the input RTL written HDL. The input HDL is subject to testing in a very recognisable manner - unit tests and integration tests that verify intended functionality. Usually with coverage reporting so you can be sure you've not forgotten areas of functionality. I feel that hardware formal verification is easier than software verification because the hardware can't be dynamically created, and there aren't weird non-local effects so it's easier to partition the problem. (Incidentally, this is the big failure flag for Ethereum: people building smart contracts without formal verification, in an environment where redeployment is extremely difficult and expensive.)
• snaky 10y ago
  There is use in software too, for critical parts mostly. Microsoft and Amazon use TLA+.