Larry said:
The software people have generally given up on the "formal proof
of correctness" concept. It turns out to be just as hard and
error-prone to set up [formal correctness] proof as it is to
write good code.
This may be true for software in general, but not for HDLs. Synopsys'
Formality and Mentor Graphics FormalPro are but 2 examples of commercial
formal verification tools. Also the development and standardization of
PSL is another example of the commitment to this concept.
Just because companies sell products and standards committees hold
meetings doesn't mean there is any lasting substance behind the concepts.
They also have a very wide use in equivalence checking, used to verify post
synthesis and post place & route tool gate level code, essential if you
don't really trust your tools!
If you don't trust your tools, _they_ did not understand the Hoare quote,
and you should switch tools. If all tools for a language are unreliable,
then the language itself is defective. How do you prove that your
equivalence checking software itself is not buggy?
This is not about making design code complicated. Good code needs to be
understandable in order to be maintainable, often overlooked. Moreover,
this is about capturing 'design intent' and provide a method of verifying
it.
Both conventional HDL and formal correctness proofs have to capture
design intent. And at some level I can understand that two different
and cross-checkable ways of expressing design intent are a Good Thing [TM].
But if the design cannot be described in a way that is "so simple that
there are obviously no deficiencies" in either paradigm, you're sunk.
Once you come up with a sensible paradigm with which to capture the design
intent, synthesize it and go on to the next project!
Of course, none of what I say argues against test benches, spot checks,
regression tests, or any other technique to exercise your code. But
the simpler the original design (or even, the simpler the initial
representation of the original design), the easier it is for such tests
to build confidence that the design _always_ does the right thing.
And the need for this, well a lot of HDL code is target at ASICs and
once committed it is neither an easy or cheap option to patch up errors.
Software on the other hand is more forgiving.
Depends. Read about the Space Shuttle software effort sometime.
- Larry