[ih] Deep dive into the C/30 microcode

[Steve Crocker]

In the mid 1980s I was working on formal proof techniques for microcode.
We used the C/30 microcode as our  "object of affection."  That is, we
wrote formal descriptions of both MBB and the C/30 instruction set (ISA),
and then set out to show that the microcode implemented the C/30 ISA when
executing on the MBB.  Attached are some crudely photographed copies of
slides I dredged out of my files.  (I can try to make a better copy if
anyone is interested.)

Since the machines were working and out in the field, we didn't expect to
find anything major.  Nonetheless, in anticipation that we might find some
rough edges, we adopted a classification system for the problems.  The
major error categories were:

A = an error in the microcode
B = an error in the description of the MBB
C = an error in the description of the C/30
D = an error or limitation in our proof system.

We broke down groups B and C into three subgroups:

B1, C1 = error in the documentation of the architecture
B2, C2 = ambiguity in the documentation of the architecture
B3, C3 = our error in creating the formal description of the architecture

There were 128 distinct opcodes.  Ten of these were for IO, maintenance or
diagnostic purposes.  We did not deal with these.  We did push through
proofs for the other 118 opcodes.  In a number of cases we found problems.
Some of these were discrepancies in the documentation or our formalization
of the architectures.  Others were actual errors in the microcode but of
little consequence because they caused inconsequential errors in the
behavior of the instruction.  A common case was returning the wrong error
code, but the code running on top of the instruction didn't make use of the
error code.

One of the more droll discrepancies were the implementations of the Set
Overflow Bit and Reset Overflow Bit instructions.  We found their
implementations were reversed.  However, when we consulted with BBN, they
said they had found the error but instead of changing the microcode, they
changed the output of the assembler.

Cheers,

Steve


















































Sent from my iPhone