3.2  Complementation

We have a simple arithmetic definition of the logical complement.

Definition 3.2.1   (lognot-def) For all $ x \in \mathbb{Z}$, $ \mathit{lognot}(x) = - x - 1$.

Notation: $ \mathit{lognot}(x)$ is abbreviated as $ \verb! !x$. For the purpose of resolving ambiguous expressions, this construction has higher precedence than the bit slice operator, e.g., $ \verb! !x[i:j] = (\verb! !x)[i:j]$.

  (lognot-shift) If $ x \in \mathbb{Z}$ and $ k \in \mathbb{N}$, then $ \verb! !(2^kx) = 2^k(\verb! !x) + 2^k - 1$.

PROOF: By Definition 3.2.1,

$\displaystyle 2^k(\verb! !x) + 2^k - 1 = 2^k(-x -1) + 2^k - 1 = -2^kx - 1 = \verb! !(2^kx). $

  (lognot-fl) If $ x \in \mathbb{Z}$, $ n \in \mathbb{N}$, and $ n > 0$, then $ \verb! !\lfloor x/n \rfloor = \lfloor\verb! !x/n \rfloor$.

PROOF: By Definition 3.2.1 and Lemma 1.1.8,

$\displaystyle \left\lfloor (\verb! !x)/n \right\rfloor = \left\lfloor \frac{-x ...
...r
= -\left\lfloor \frac{x}{n} \right\rfloor - 1 = \verb! !\lfloor x/n \rfloor. $

  (mod-lognot) If $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$, $ \verb! !x \bmod 2^n = 2^n - (x \bmod 2^n) - 1$.

PROOF: First note that by Lemmas 1.2.2 and 1.2.3, $ 0 \leq 2^n - (x \bmod 2^n) - 1 < 2^n$. Therefore, by Lemmas 1.2.15, 1.2.19, and 1.2.6,

$\displaystyle \verb! !x \bmod 2^n = (-x - 1) \bmod 2^n = (2^n - (x \bmod 2^n) - 1) \bmod 2^n = 2^n - (x \bmod 2^n) - 1. $

  (bits-lognot) If $ x \in \mathbb{Z}$, $ i \in \mathbb{N}$, $ j \in \mathbb{N}$, and $ j \leq i$, then $ \verb! !x[i:j] = 2^{i+1-j} - x[i:j] - 1$.

PROOF: By Definitions 3.2.1 and 2.0.1 and Lemmas 3.2.3, 1.1.4, and 1.1.8,

$\displaystyle \verb! !x[i:j]$ $\displaystyle =$ $\displaystyle \left\lfloor (\verb! !x \bmod 2^{i+1})/2^j \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{2^{i+1} - (x \bmod 2^{i+1}) - 1}{2^j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle \frac{2^{i+1}}{2^j} + \left\lfloor -\frac{(x \bmod 2^{i+1}) + 1}{2^j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle 2^{i+1-j} - \left\lfloor \frac{x \bmod 2^{i+1}}{2^j} \right\rfloor - 1$  
  $\displaystyle =$ $\displaystyle 2^{i+1-j} - x[i:j] - 1. $  

The primary property of the complement is a special case of Lemma 3.2.4:

  (bitn-lognot) If $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$, then $ \verb! !x[n] \neq x[n]$.

PROOF: By Lemma 3.2.4, $ \verb! !x[n] = 2^{n+1-n} - x[n] - 1 = 1 - x[n]$


The remaining result of this section are properties of complements of bit slices that have proved useful in manipulating expressions derived from RTL designs.

  (bits-lognot-bits) Let $ x \in \mathbb{Z}$, $ i \in \mathbb{N}$, $ j \in \mathbb{N}$, $ k \in \mathbb{N}$, and $ \ell \in \mathbb{N}$. If $ \ell \leq k \leq i-j$, then

$\displaystyle \verb! !(x[i:j])[k:\ell] = \verb! !x[k+j:\ell+j].
$

PROOF: By Lemmas 3.2.4 and 2.2.23,

$\displaystyle \verb! !(x[i:j])[k:\ell]$ $\displaystyle =$ $\displaystyle 2^{k+1-\ell} - x[i:j][k:\ell] - 1$  
  $\displaystyle =$ $\displaystyle 2^{(k+j)+1-(\ell+j)} - x[k+j:\ell+j] - 1$  
  $\displaystyle =$ $\displaystyle \verb! !x[k+j:\ell+j]. $  

  (bits-lognot-bits-lognot) Let $ x \in \mathbb{Z}$, $ i \in \mathbb{N}$, $ j \in \mathbb{N}$, $ k \in \mathbb{N}$, and $ \ell \in \mathbb{N}$. If $ \ell \leq k \leq i-j$, then

$\displaystyle \verb! !(\verb! !x[i:j])[k:\ell] = x[k+j:\ell+j].
$

PROOF: By Lemmas 3.2.4 and 2.2.23,

$\displaystyle \verb! !(\verb! !x[i:j])[k:\ell]$ $\displaystyle =$ $\displaystyle 2^{k+1-\ell} - \verb! !x[i:j][k:\ell] - 1$  
  $\displaystyle =$ $\displaystyle 2^{(k+j)+1-(\ell+j)} - \verb! !x[k+j:\ell+j] - 1$  
  $\displaystyle =$ $\displaystyle \verb! !(\verb! !x)[k+j:\ell+j],$  

where $ \verb! !(\verb! !x) = -(-x - 1) - 1 = x$

  (logand-bits-lognot) If $ x \in \mathbb{Z}$ and $ y$ in an $ n$-bit vector, where $ n \in \mathbb{N}$, then

$\displaystyle \verb! !(x[n-1:0]) \;\verb!&!\; y = \verb! !x[n-1:0] \;\verb!&!\; y.
$

PROOF: By Lemma 3.2.6, $ \verb! !(x[n-1:0])[n-1:0] = \verb! !x[n-1:0]$, and hence by Lemmas 3.1.2, 2.2.5, and 3.1.13

$\displaystyle \verb! !(x[n-1:0]) \;\verb!&!\; y = \left(\verb! !(x[n-1:0]) \;\v...
...b! !(x[n-1:0])[n-1:0] \;\verb!&!\; y[n-1:0]
= \verb! !x[n-1:0] \;\verb!&!\; y. $

David Russinoff 2017-08-01