[Author Prev][Author Next][Thread Prev][Thread Next][Author Index][Thread Index]
Re: [f-cpu] Verification, Testing, And Random Numbers
Hi!
Just an Illusion wrote:
[...]
I am not totally agree with you about tools, some are announce like
functional symbolic verification, but in fact they doesn't well work.
That's what we call "Etikettenschwindel" in Germany: the label on the
box says A, but the box contains B (or maybe Z)...
The functional symbolic verification is not the only way, you have the
model checkers, like proof checkers, which do the same.
More or less, yes.
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.
BDDs will "explode" when the operands' width grows. For (integer) adders
and multipliers, *BMDs (multiplicative binary moment diagrams) are
preferable because they don't. And in contrast to BDDs, they can
represent (integer) numbers. That makes verification rather easy - just
compare the pointers.
*BMDs (or similar constructs) don't work with division, though.
Michael.
*************************************************************
To unsubscribe, send an e-mail to majordomo@seul.org with
unsubscribe f-cpu in the body. http://f-cpu.seul.org/