3 ms·

edit: just to be clear, I'm responding to this statement: > Formal verification does take more time over empirical testing methods I don't even know if that i

by wsxcde 12y ago

edit: just to be clear, I'm responding to this statement: > Formal verification does take more time over empirical testing methods I don't even know if that is true, at least, I'm unconvinced about it being true in hardware verification. The amount of manpower and effort companies like Intel and AMD put into simulation-based verification is insane and a lot of that could be replaced (and has in some case been replaced) by a well-designed formal assertion suite. The real bottleneck is people. It's a lot easier to find competent engineers who can hack around with tests and simulation suites than it is to find people who can hack around with abstractions for scalability in a model checker.

nanolith 12y ago
There is a pragmatic perspective and a theoretic perspective. Pragmatically speaking, empirical methods can get one pretty far. It's better to have full coverage of empirical tests across an entire system than limited coverage of formal tests, for instance. So, on that account, you may be correct from a pragmatic perspective. From an epistemological perspective, a test suite to confirm a property using chosen examples is not nearly as good as a formal proof that guarantees a property over a given domain. For simple cases, such as branch coverage, the test suite may be good enough. As complexity increases, or when testing things like modular arithmetic over an elliptic curve, unit testing leads to false confidence. But, just like in empirical testing, it's possible to build bad proofs. This is where the specialization comes in. There may be plenty of competent engineers who can hack at a test suite, but their results will not be nearly as comprehensive as someone trained in formal verification. It all comes down to epistemology. What do we know, and how do we know it? What possible defects exist in our system, and how bad can they be? Can we ship yet?
- nullc 12y ago
  Any kind of testing or review can lead to false confidence. This is why its important to use multiple approaches in the hope that their errors are not completely correlated.
  - nanolith 12y ago
    I agree.

by wsxcde 12y ago

nanolith 12y ago

There is a pragmatic perspective and a theoretic perspective. Pragmatically speaking, empirical methods can get one pretty far. It's better to have full coverage of empirical tests across an entire system than limited coverage of formal tests, for instance. So, on that account, you may be correct from a pragmatic perspective. From an epistemological perspective, a test suite to confirm a property using chosen examples is not nearly as good as a formal proof that guarantees a property over a given domain. For simple cases, such as branch coverage, the test suite may be good enough. As complexity increases, or when testing things like modular arithmetic over an elliptic curve, unit testing leads to false confidence. But, just like in empirical testing, it's possible to build bad proofs. This is where the specialization comes in. There may be plenty of competent engineers who can hack at a test suite, but their results will not be nearly as comprehensive as someone trained in formal verification. It all comes down to epistemology. What do we know, and how do we know it? What possible defects exist in our system, and how bad can they be? Can we ship yet?

nullc 12y ago
Any kind of testing or review can lead to false confidence. This is why its important to use multiple approaches in the hope that their errors are not completely correlated.
- nanolith 12y ago
  I agree.