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

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


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.


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