A common task performed by floating-point units is the conversion of an encoding from one format to another, which generally requires the rebiasing of the exponent field. If is the value of an exponent field of width , then the actual exponent of the encoded number is . The result of rebiasing this value for a field of width is given by the following definition.
When the target exponent field is wider than that of the source, rebiasing is always possible.
PROOF: First suppose that . Then by Lemmas 2.2.5 and 2.3.17,
Now suppose that is an -bit biased exponent to be rebiased to fit into a smaller -bit field. In order for this to be possible,
PROOF: The hypothesis implies that is an -bit vector, and hence, by Lemmas 2.2.5, 2.3.17, and 2.2.22,
David Russinoff 2017-08-01