SiFive developed the floating point unit in a modeling language named Chisel. I began by writing a set of recurrence relations that formalized the square root and division algorithms. I then identified bijective mappings between the variables used in SiFive's model and the variables used in my equations. This allowed me to prove that my equations correctly modeled the unit. Then, I verified that my equations correctly converged onto the correct results, thereby verifying that SiFive's unit was logically correct.

One problem remained however. SiFive's unit defined a register named \(rem\), and they feared that this register was too small to store all of the intermediate values computed during operation. To prove that the \(rem\) register was large enough, I needed to prove that the values stored within \(rem\) were smaller than \(2^w\), where \(w\) represented the number of bits SiFive had allocated.

This register corresponded to a variable defined within my equations named \(error(n)\). Using the mapping between \(rem\) and \(error(n)\), I had to verify that: $$\forall n, error(n) < \frac{8}{2^n}$$ when computing the square root of an odd number, and an analogous result when computing the square root of even numbers. The following is an extract of my proof of this result.

Let \(x\) denote the number that the floating point unit is computing the square root for. Let \(approx(n)\) denote the \(n^{th}\) approximation of the square root of \(x\). And, let \(error(n)\) represent the \(n^{th}\) approximation error. Then \(x\) is given by:

Setting \(approx(0) = 0\), we will append a bit, \(b(n)\), onto the approximation at the end of each iteration.

where:

Using back substitution we can solve for \(error\) to derive the following recurrence relation:

Using the above equations and the fact that \(1 <= x < 2\), we can derive the following corollaries:

Proof

We proceed using a proof by induction. When n = 0, substitution gives:

When \(n \gt 0\), we have to prove:

We proceed by case analysis. \(b (n)\) equals either 0 or 1.

b (n) = 0

When \(b (n) = 0\), our goal becomes: \(x \lt (approx (n) + \frac{1}{2^n})^2\). Expanding and rewriting \(error\) using (7) leads to:

b (n) = 1

When \(b (n) = 1\), our goal becomes: \(x \lt (approx (n) + \frac{1}{2^n} + \frac{1}{2^n})^2\). However, this is equivalent to: \(a \lt (approx (n) + \frac{2}{2^n})^2\), which is identical to our inductive hypothesis. ∎

Proof

We proceed using proof by induction.

n = 0

When \(n = 0\), the lemma follows immediately from (5): \(error (0) = x \lt 2\).

n ≥ 1

When \(n \ge 1\), our goal becomes: \(error (n) \lt 4 \implies\)\(error (n + 1) \lt 4\). Assuming that \(error (n) \lt 4\) and expanding \(error (n + 1)\) leads to:

Where we maximized the rhs in the last inequality by taking the case where \(b (n) = 0\). ∎

Derivation

Corollary 1.4 follows algebraically from Lemma 1.1:

Proof

We will proceed using induction over \(n\). When \(n = 0\), \(error (0) = x \lt 2\) and Theorem 1.4 follows immediately. Hence, we only need to consider the case where \(n \ge 1\).

Observe that:

We can substitute this upper bound into the scaling upper bound we derived in Corollary 1.3. Doing so leads to:

which is always less than \(\frac{8}{2^n}\) when \(n \ge 1\). This observation completes this proof. ∎