Hi,
I have question reagrds the signatures:

if I have two functions: f1(x1,x2,x3) and f2(x1,x2,x3), and the signature are:

1-for f1, the signatures are as follows:

x1=2
x2=4
x3=7

2-for f2, the signature are as follows:

x1=4
x2=2
x3=8

so the signature are not "paarweise verschieden", the question is that the two functions have not the same characteristics and functionality and the ROBDD for both of them are different?


this means that before make any Equivalence Test between implemenation and specification, we need to check the signatures, if they have different values then there is no need any more for building ROBDD and checking the equivalence?

All thanks.