6 Aug
2018
6 Aug
'18
5:18 a.m.
On Thu, 02 Aug 2018 08:44:56 -0400 Doug McIlroy
<doug(a)cs.dartmouth.edu> wrote:
A tangential connection to early Unix experience:
My collection of early computer manuals includes Brinch Hansen's
manual for the RC 4000, which stands out for its precise
description of the CPU logic--in Algol 60! It's the only manual I
have seen that offers a good-to-the-last-bit formal description of
the hardware.
DEC presented something of the sort for the PDP-11, but punted where
the woods got thick. When I wanted to know how they computed the
last bit of floating-point results, I got no satisfaction. Amidst a
thorough description of addressing came this formulation of the
actual computation: "form floating point result".
For those that are familiar with the RISC V architecture, there's a
formal specification of the architecture that was done in a system
built on Coq, and also a fully formally verified translation of the
specification into RTL. (The spec didn't include floating point as of
about a year ago but it may by now.)
A good overview of the system involved is here:
http://plv.csail.mit.edu/kami/papers/icfp17.pdf
Followups might belong on the coff list, not sure.
Perry
--
Perry E. Metzger perry(a)piermont.com