1.3  Chop

The following function, which relates to the fixed-point registers defined in Part V, truncates a real number to a specifed numebr of fractional bits:

Definition 1.3.1   (chop) For $ x \in \mathbb{R}$ and $ k \in \mathbb{Z}$,

$\displaystyle \mathit{chop}(x, k)= \frac{\lfloor 2^{k}x \rfloor}{2^{k}}.
$

Notation: We shall abbreviate $ \mathit{chop}(x, k)$ as $ x^{(k)}$.

  (chop-mod) For $ x \in \mathbb{R}$ and $ k \in \mathbb{Z}$,

$\displaystyle x^{(k)} = x - x \bmod 2^{-k}
$

PROOF: This is an instance of Definition 1.2.1

  (chop-chop) If $ x \in \mathbb{R}$, $ m \in \mathbb{Z}$, $ k \in \mathbb{Z}$, and $ k \leq m$, then

$\displaystyle \left(x^{(k)}\right)^{(m)} = \left(x^{(m)}\right)^{(k)} = x^{(k)}.
$

PROOF:

$\displaystyle \left(x^{(k)}\right)^{(m)} = \left(\frac{\lfloor 2^kx \rfloor}{2^...
...2^{m-k}\lfloor 2^kx \rfloor}{2^m} = \frac{\lfloor 2^kx \rfloor}{2^k} = x^{(k)}
$

and

$\displaystyle \left(x^{(m)}\right)^{(k)} = \left(\frac{\lfloor 2^mx \rfloor}{2^...
...^mx}{2^{m-k}}\right\rfloor}{2^k} = \frac{\lfloor 2^kx \rfloor}{2^k} = x^{(k)}. $

  (chop-shift) If $ x \in \mathbb{R}$, $ m \in \mathbb{Z}$, and $ k \in \mathbb{Z}$, then

$\displaystyle (2^kx)^{(m)} = 2^kx^{(k+m)}.
$

PROOF: $ (2^kx)^{(m)} = 2^{-m}\lfloor 2^m(2^kx)\rfloor = 2^k(2^{-(k+m)}\lfloor 2^{k+m}x\rfloor = 2^kx^{(k+m)}.$ 

  (chop-bound) If $ x \in \mathbb{R}$, $ m \in \mathbb{N}$, $ n \in \mathbb{Z}$, then $ n \leq x \Leftrightarrow n \leq x^{(m)}$.

PROOF: $ n \leq x \Leftrightarrow 2^mn \leq 2^mx \Leftrightarrow 2^mn \leq \lfloor 2^mx \rfloor
\Leftrightarrow n \leq \frac{\lfloor 2^mx \rfloor}{2^m}$

  (chop-small) If $ x \in \mathbb{R}$, $ m \in \mathbb{Z}$, and $ -2^{-m} \leq x < 2^{-m}$, then

$\displaystyle x^{(m)} = \left\{\begin{array}{cl}
0 & \mbox{if $x \geq 0$}\\
-2^{-m} & \mbox{if $x < 0$.}\end{array}\right.
$

PROOF: Since $ -1 \leq 2^mx < 1$, $ -1 \leq \lfloor 2^mx \rfloor < 1$, which implies

$\displaystyle \lfloor 2^mx \rfloor = \left\{\begin{array}{rl}
0 & \mbox{if $x \geq 0$}\\
-1 & \mbox{if $x < 0$}\end{array}\right.
$

and

$\displaystyle x^{(m)} = 2^{-m}\lfloor 2^mx \rfloor = \left\{\begin{array}{cl}
...
...f $x \geq 0$}\\
-2^{-m} & \mbox{if $x < 0$. \mbox{$\Box$}}\end{array}\right.
$

  (chop-0) If $ x \in \mathbb{R}$, $ m \in \mathbb{Z}$, and $ -2^{-m} < x^{(m)} < 2^{-m}$, then $ x^{(m)} = 0$.

PROOF: $ -1 < \lfloor 2^mx \rfloor < 1 \Rightarrow \lfloor 2^mx \rfloor = 0 \Rightarrow x^{(m)} = 0$


Notation: We shall abbreviate $ \mathit{chop}(x, -k)$ as $ x^{\langle k \rangle}$.

If $ k>0$, then $ x^{\langle k \rangle} = 2^{k}\lfloor 2^{-k}x\rfloor$ is the largest multiple of $ 2^{k}$ that does not exceed $ x$. The following lemmas have found application in the analysis of floating-point adders.

  (chop-int-bounds) If $ k \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ x \in \mathbb{R}$, then

(a) $ \left\lfloor \frac{x}{2^n} \right\rfloor^{\langle k \rangle} \leq \frac{x^{\langle k \rangle}}{2^n}$;

(b) $ \frac{x^{\langle k \rangle} + 2^k}{2^n} \leq \left\lfloor \frac{x}{2^n} \right\rfloor^{\langle k \rangle} + 2^{k}$.

PROOF:

(a) By Lemma 1.1.5,

$\displaystyle \left\lfloor \frac{x}{2^n} \right\rfloor^{\langle k \rangle}$ $\displaystyle =$ $\displaystyle 2^k\left\lfloor \frac{\left\lfloor \frac{x}{2^n} \right\rfloor}{2^k}\right\rfloor$  
  $\displaystyle =$ $\displaystyle 2^k\left\lfloor \frac{x}{2^{k+n}} \right\rfloor$  
  $\displaystyle =$ $\displaystyle 2^k\left\lfloor \frac{\left\lfloor \frac{x}{2^k} \right\rfloor}{2^n}\right\rfloor$  
  $\displaystyle \leq$ $\displaystyle 2^k \frac{\left\lfloor \frac{x}{2^k} \right\rfloor}{2^n}$  
  $\displaystyle =$ $\displaystyle \frac{x^{\langle k \rangle}}{2^n}.$  

(b) By Lemmas 1.2.1, 1.2.3, and 1.1.5,


$\displaystyle \frac{x^{\langle k \rangle} + 2^k}{2^n}$ $\displaystyle =$ $\displaystyle \frac{2^k\left(\left\lfloor \frac{x}{2^k}\right\rfloor + 1\right)}{2^n}$  
  $\displaystyle =$ $\displaystyle 2^{k-n}\left(\left\lfloor \frac{x}{2^k}\right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle 2^{k-n}\left(2^n\left\lfloor \frac{\left\lfloor \frac{x}{2^k}\rig...
...n}\right\rfloor
+ \left\lfloor \frac{x}{2^k}\right\rfloor \bmod {2^n}+ 1\right)$  
  $\displaystyle \leq$ $\displaystyle 2^{k-n}\left(2^n\left\lfloor \frac{\left\lfloor \frac{x}{2^k}\right\rfloor}{2^n}\right\rfloor + (2^n-1)+ 1\right)$  
  $\displaystyle =$ $\displaystyle 2^k\left(\left\lfloor \frac{\left\lfloor \frac{x}{2^n}\right\rfloor}{2^k}\right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^n} \right\rfloor^{\langle k \rangle} + 2^{k}. $  

  (chop-int-neg) Let $ k \in \mathbb{N}$, $ n \in \mathbb{N}$, $ x \in \mathbb{R}$, and $ y \in \mathbb{R}$. $ y = x^{\langle k \rangle}$. If $ \lfloor 2^{-k}x \rfloor = \lfloor 2^{-k}y \rfloor$ and $ 2^{-k}x \notin \mathbb{Z}$, then

$\displaystyle \left(-\left\lfloor \frac{y}{2^n} \right\rfloor -1\right)^{\langle k \rangle} =
\left(-\frac{x}{2^n}\right)^{\langle k \rangle}.
$

PROOF: We simplify the expression on the left using Lemmas 1.1.5 and 1.1.8:

$\displaystyle \left(-\left\lfloor \frac{y}{2^n} \right\rfloor -1\right)^{\langle k \rangle}$ $\displaystyle =$ $\displaystyle 2^k\left\lfloor -\frac{\left\lfloor \frac{y}{2^n} \right\rfloor + 1}{2^k} \right\rfloor$  
  $\displaystyle =$ $\displaystyle -2^k\left(\left\lfloor \frac{\left\lfloor \frac{y}{2^n} \right\rfloor}{2^k} \right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle -2^k\left(\left\lfloor \frac{\left\lfloor \frac{y}{2^k} \right\rfloor}{2^n} \right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle -2^k\left(\left\lfloor \frac{\left\lfloor \frac{x}{2^k} \right\rfloor}{2^n} \right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle -2^k\left(\left\lfloor \frac{x}{2^{k+n}} \right\rfloor + 1\right)$  

For the expression on the right, we apply the same two lemmas and Lemma 1.1.7:
$\displaystyle \left(-\frac{x}{2^n}\right)^{\langle k \rangle}$ $\displaystyle =$ $\displaystyle 2^k\left\lfloor -\frac{\frac{x}{2^n}}{2^k} \right\rfloor$  
  $\displaystyle =$ $\displaystyle 2^k\left\lfloor \frac{-x}{2^{k+n}} \right\rfloor$  
  $\displaystyle =$ $\displaystyle 2^k\left\lfloor \frac{\left\lfloor \frac{-x}{2^k} \right\rfloor}{2^n}\right\rfloor$  
  $\displaystyle =$ $\displaystyle 2^k\left\lfloor \frac{-\left\lfloor \frac{x}{2^k} \right\rfloor - 1}{2^n}\right\rfloor$  
  $\displaystyle =$ $\displaystyle -2^k\left(\left\lfloor \frac{\left\lfloor \frac{x}{2^k} \right\rfloor}{2^n} \right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle -2^k\left(\left\lfloor \frac{x}{2^{k+n}} \right\rfloor + 1\right)$  
  $\displaystyle =$ $\displaystyle \left(-\left\lfloor \frac{y}{2^k} \right\rfloor -1\right)^{\langle k \rangle}. $  

David Russinoff 2017-08-01