3.2  Complementation

We have a simple arithmetic definition of the logical complement.

Definition 3.2.1   (lognot-def) For all , .

Notation: is abbreviated as . For the purpose of resolving ambiguous expressions, this construction has higher precedence than the bit slice operator, e.g., .

PROOF: By Definition 3.2.1,

PROOF: By Definition 3.2.1 and Lemma 1.1.8,

PROOF: First note that by Lemmas 1.2.2 and 1.2.3, . Therefore, by Lemmas 1.2.15, 1.2.19, and 1.2.6,

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

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

PROOF: By Lemma 3.2.4,

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

PROOF: By Lemmas 3.2.4 and 2.2.23,

PROOF: By Lemmas 3.2.4 and 2.2.23,

where

(logand-bits-lognot) If and in an -bit vector, where , then

PROOF: By Lemma 3.2.6, , and hence by Lemmas 3.1.2, 2.2.5, and 3.1.13

David Russinoff 2017-08-01