Most significant bit of integer multiplication and binary decision diagrams Let $x$ and $y$ two binary numbers with $n$ bits and $z = x \cdot y\ $ the binary number (length $2n$) of the product of $x$ and $y$. We want to compute the most siginifcant bit $z_{2n-1}$ of the product $z = z_{2n-1} \ldots z_0$.

In order to analyse the complexity of this function in the model of binary decision diagrams (in particular read-once branching programs) I try to look for some equivalent expressions for the case $z_{2n-1} = 1$. The first obvious thing is $z_{2n-1} = 1 \Leftrightarrow x \cdot y \geq 2^{2n-1}$ (here $x$ and $y$ are the corresponding integers to the binary numbers). I want to get an intuition what happens if I set some input bits constant. E.g. if I set the most significant input bit from $x$ and $y$ to 0 I get the constant 0 function. But bits with lower significance haven't such an influence on the result.

Are there any other equivalent expressions for the case $z_{2n-1} = 1$ which help more to see what happens if I fix some input bits? Are there any refined methods to compute the product of two binary numbers which can help? Or do you have some other approach to this problem?
An interesting source is D. E. Knuth: The Art of Computer Programming, Volume 4, Fascicle 1, Bitwise Tricks &amp; Techniques; Binary Decision Diagrams, Addison-Wesley, Pearson Education 2009

On page 96, there is a BDD for all bits of z = x⋅y, where x and y have 3 bits. It shows, that in the case of 3 bits, BDD representing the most significant bit has 7 non-terminal nodes. See the image bellow, I have redraw it using your indices x = (x2,x1,x0) and y = (y2,y1,y0).

On page 140 in Knuth's book, there is a question (no. 183) about BDD representing the most significant bit for multiplication of two numbers with infinitely many bits (it is called "limiting leading bit function") - this is similar to what you are loking for! The answer on page 223 gives first levels of the resulting BDD and discusses the number of nodes on all levels, but unfortunatelly it does not give algorithm to construct such a BDD.



Fig. 1: The most significant bit for multiplication of (x2,x1,x0) * (y2,y1,y0)