[Author Prev][Author Next][Thread Prev][Thread Next][Author Index][Thread Index]

Re: [f-cpu] Verification, Testing, And Random Numbers


Michael Riepe wrote:

For a), you have to verify that a unit does what it is supposed to do: adders shall add, multipliers shall multiply and so on. There are several methods to do that...

Functional symbolic verification would be the real thing. It transforms both the operands and the result into a special representation (using BDDs oder one of their derivatives), performs the operation in either representation, and compares the results. You need only a single run per operation, and the result is as reliable as that of an exhaustive test, only much faster. But there are no tools for it (yet).
I am not totally agree with you about tools, some are announce like functional symbolic verification, but in fact they doesn't well work.
The functional symbolic verification is not the only way, you have the model checkers, like proof checkers, which do the same.

But in any case, all this tools and methods are well suitable for control-path models verification. The bdd (binary decision diagram) or other representation found quickly their limits, when the model is more data-path like adder or multiplier. Their limits are intrinsic to the mathematical theory use to solve the equations.


To unsubscribe, send an e-mail to majordomo@seul.org with
unsubscribe f-cpu in the body. http://f-cpu.seul.org/