3 ms·

SQLite is usually (and correctly) held as an example of thorough software testing: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html Perh

by nkurz 11y ago

SQLite is usually (and correctly) held as an example of thorough software testing: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html Perhaps you could offer a sense of how this compares to the hardware testing practices you use?

whaaswijk 11y ago
Typically in hardware design you'd use combinational equivalence checking (CEC) to formally prove that a synthesized design is correct. See https://en.wikipedia.org/wiki/Formal_equivalence_checking https://en.wikipedia.org/wiki/Formal_equivalence_checking. In CEC you use a SAT solver to prove that a new (synthesized and optimized) circuit is equivalent to some reference model (aka golden model) which you know is correct. So instead of relying on just testing (which is incomplete) you have a formal proof that your design is correct. Of course you still have to trust that the SAT solver works correctly... :-)
StringyBob 11y ago
In hardware design you typically test functionality through logic simulation or emulation (effectively running the code in a computer simulation or fpga), use test harnesses, look for code coverage, run unit tests, random code fuzzing, code assertions etc. You might also do formal checks for some assertions to e.g. avoid deadlocks. A secondary check is that the source that you functionally tested is logically equivalent to what you manufacture. This is where you are not checking your code, but the issue is trust of compiler/ compiler optimisations in synthesis. It needs to be redone if you recompile - that's the step I don't really ever see in software development - if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? Of course the level of paranoia is far higher in hardware where it costs multiple millions of dollars to crank out a new spin of a chip!
- dalke 11y ago
  > if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? If that is critical, you can join the SQLite Consortium Membership for $75K/year and access to the test suite. There's also an option to pay SQLite developers to "run TH3 on specialized hardware and/or using specialized compile-time options, according to customer specification, either remotely or on customer premises." The TH3 test harness is an aviation-grade test suite. The level of paranoia for aviation software is also rather high.

by nkurz 11y ago

whaaswijk 11y ago

Typically in hardware design you'd use combinational equivalence checking (CEC) to formally prove that a synthesized design is correct. See https://en.wikipedia.org/wiki/Formal_equivalence_checking https://en.wikipedia.org/wiki/Formal_equivalence_checking. In CEC you use a SAT solver to prove that a new (synthesized and optimized) circuit is equivalent to some reference model (aka golden model) which you know is correct. So instead of relying on just testing (which is incomplete) you have a formal proof that your design is correct. Of course you still have to trust that the SAT solver works correctly... :-)

StringyBob 11y ago

In hardware design you typically test functionality through logic simulation or emulation (effectively running the code in a computer simulation or fpga), use test harnesses, look for code coverage, run unit tests, random code fuzzing, code assertions etc. You might also do formal checks for some assertions to e.g. avoid deadlocks. A secondary check is that the source that you functionally tested is logically equivalent to what you manufacture. This is where you are not checking your code, but the issue is trust of compiler/ compiler optimisations in synthesis. It needs to be redone if you recompile - that's the step I don't really ever see in software development - if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? Of course the level of paranoia is far higher in hardware where it costs multiple millions of dollars to crank out a new spin of a chip!

dalke 11y ago
> if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? If that is critical, you can join the SQLite Consortium Membership for $75K/year and access to the test suite. There's also an option to pay SQLite developers to "run TH3 on specialized hardware and/or using specialized compile-time options, according to customer specification, either remotely or on customer premises." The TH3 test harness is an aviation-grade test suite. The level of paranoia for aviation software is also rather high.