3 ms·

Formal methods are particularly effective for verifying hardware, because a) the state space is much smaller than for software (although it can still be prohibi

Formal methods are particularly effective for verifying hardware, because 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) b) people are actually ready to shell out some decent money for getting the verification done.

baybal2 9y ago
>people are actually ready to shell out some decent money for getting the verification done. 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.
throwaway40483 9y ago
Not only is formal methods more effective for HW, the incentives are also more tilted towards HW. If you fuck up the HW design, well..you're fucked. With SW, "you can always push out an update" mentality exists. I'm not saying this to criticize SW, but this is more an example of how you conform to the ecosystem in which you exist.
- DennisP 9y ago
  Which is why people are keen on developing formal methods for smart contracts, which generally can't be updated. Plus they're a lot smaller than most software.
Nokinside 9y ago
d) specifications are more explicit and they can be frozen. Once the module is verified it can be reused, justifying the cost. There are only few software products that are formally verified. Some data diodes and real time operating systems (at least partially).
- pron 9y ago
  > There are only few software products that are formally verified. 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.
pron 9y ago
> b) people are actually ready to shell out some decent money for getting the verification done. 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.
pedroaraujo 9y ago
Even in hardware, formal verification is only used for really small designs (like FIFOs, for example) and for very specific and simplistic designs (control logic or datapaths). For everything else, people use the good old functional verification because more the state complexity of more complex designs simply explodes.
- Cyph0n 9y ago
  Heck, even a cache coherence protocol can't be formally verified. Imagine trying to verify an entire CPU...

baybal2 9y ago

>people are actually ready to shell out some decent money for getting the verification done. 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.

throwaway40483 9y ago

Not only is formal methods more effective for HW, the incentives are also more tilted towards HW. If you fuck up the HW design, well..you're fucked. With SW, "you can always push out an update" mentality exists. I'm not saying this to criticize SW, but this is more an example of how you conform to the ecosystem in which you exist.

DennisP 9y ago
Which is why people are keen on developing formal methods for smart contracts, which generally can't be updated. Plus they're a lot smaller than most software.

Nokinside 9y ago

d) specifications are more explicit and they can be frozen. Once the module is verified it can be reused, justifying the cost. There are only few software products that are formally verified. Some data diodes and real time operating systems (at least partially).

pron 9y ago
> There are only few software products that are formally verified. 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.

pron 9y ago

> b) people are actually ready to shell out some decent money for getting the verification done. 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.

pedroaraujo 9y ago

Even in hardware, formal verification is only used for really small designs (like FIFOs, for example) and for very specific and simplistic designs (control logic or datapaths). For everything else, people use the good old functional verification because more the state complexity of more complex designs simply explodes.

Cyph0n 9y ago
Heck, even a cache coherence protocol can't be formally verified. Imagine trying to verify an entire CPU...