[Author Prev][Author Next][Thread Prev][Thread Next][Author Index][Thread Index]
Re: [f-cpu] Verification, Testing, And Random Numbers
Hi,
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.
Bye,
JaI
*************************************************************
To unsubscribe, send an e-mail to majordomo@seul.org with
unsubscribe f-cpu in the body. http://f-cpu.seul.org/