Jtdylktuy

In this book, sections 9.4 and 10.2 explains how to implement the booth encoding to speed up operations in hardware. I've being searching for some reference for a formal proof of why this encoding is correct. I understand the rationale behind such enconding, but I don't understand why for radix greater than 2 it work.

For example, consider a number

$$
x = -x_{n-1}2^{n-1} + sum_{j=0}^{n-2} x_j 2^j
$$

The booth encoding, radix $2$ consist in defining the digits

$$
y_j = -x_j + x_{j-1} ;; 0 leq j leq n - 1
$$

In radix $4$ it becomes ($j$ is multiple of 2)

$$
y_{j/2} = -2x_{j+1} + x_j + x_{j-1}
$$

In radix $8$ ($j$ is multiple of $3$)

$$
y_{j/3} = -4x_{j+2} + 2x_{j+1} + x_j + x_{j-1}
$$

In radix $16$ ($j$ is multiple of 4)

$$
y_{j/4} = -8x_{j+3} + 4x_{j+2} + 2x_{j+1} + x_j + x_{j-1}
$$

Etc...
But I cannot work out how to prove that basically the transformation is invertible...
I'm neither sure how to problem has to be set up in order to prove that the transformation is invertible, could you help me?

What I'm sure about is that the transformation that allow me to get the digit $y_j$ is linear, so maybe I could set up some linear system.

I want to formalize this think because it is very easy to get intuition that motivate the radix $2$ booth encoding, but increasing the radix makes me lose such intuition...

My attempt to formalize the problem is the following. Let's define $r = 2^k$ then

$$
y = sum_{
left{
begin{array}{l}
i=0\
j=ki
end{array}
right.}^{m - 1} y_{j/k} 2^{ik}
$$

where

$$
y_{j/k} = -x_{j+k-1}2^{k-1} + sum_{l=0}^{k-2} x_{j+l} 2^{l} + x_{j-1}
$$

However I firstly don't know how to find the value $m$, and also I'm confused on how I can use the expansion of $y$ in terms of $y_{j/k}$ to retrieve the digits of $x$.

Update: Maybe this could work (I'm changing a bit the notation)

Let's start with radix $2$ we have

$$
sum_{j=0}^{n-1} x_j 2^j = sum_{j=0}^n left(-x_j+x_{j-1}right)2^j = sum_{j=0}^n y^1_j 2^j
$$

where

$$
y^1_j = -x_j + x_{j-1} ;,; 0 leq j leq n
$$

where $x_n = x_{-1} = 0$

Let's move to higher radix now, for radix $4=2^2$ we need to consider the digits obtained as

$$
y^2_j = y^1_{2j+1} 2 + y^1_{2j} = -2x_{2j+1} + x_{2j} + x_{2j-1} ;,; 0 leq j leq leftlceil frac{n-1}{2} rightrceil
$$

For radix $8=2^3$ we consider instead

$$
y^3_j = y^1_{3j+2} 4 + y^1_{3j+1}2 + y_{3j} = -4x_{3j+2} + x_{3j+1}2 + x_{3j} + x_{3j-1} ;,; 0 leq j leq leftlceil frac{n-2}{3} rightrceil
$$

In general, i.e. radix $2^k$ we have

$$
begin{multline}
y^k_j = y^1_{kj + k - 1} 2^{k-1} + y^1_{kj + k - 2} 2^{k-2} + ldots + y^1_{kj} = \
-x_{kj+k-1}2^{k-1} + x_{kj + k - 2} 2^{k-2} + ldots + x_{kj} + x_{kj-1} = \
;,; 0 leq j leq leftlceil frac{n-k+1}{k} rightrceil
end{multline}
$$

Is this sufficient to state that

$$
x = sum_{j=0}^{n} x_j 2^j = sum_{j=0}^{leftlceil frac{n-k+1}{k}rightrceil} y_j^k 2^j
$$