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

[Michael Riepe <michael+fcpu@stud.uni-hannover.de>]

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/