Most significant bit of integer multiplication and binary decision diagrams
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)