gvw@uunet.UU.NET (11/04/88)
I am writing in response to your recent posting in comp.society.women.
During the design of the INMOS T800 chip, formal mathematical methods
were used to prove that microcode for the chip's floating point unit
would behave correctly. This cut design time so much (more than half,
less than an order of magnitude) that INMOS are now expanding their use
of formal methods to encompass the whole chip-design process.
Their eventual CAD system will include mathematical specifications of
behaviour of circuit components along with the hardware descriptions of the
circuit components themselves. Chips will then be specified by producing
a description of how they are behave; designers will lay the chip out,
and then work backward from the mathematical information contained in
the CAD library to prove that the chip meets the specification.
So why is this interesting? Well, constructing an internally-consistent
specification is just like creating any other axiomatic description
in mathematics, while proving that a chip design meets its spec is the
sort of thing mathematical training is supposed to teach someone to do.
The T800 design team included a couple of mathematicians, out of fewer
than 10 full-time staff; work on the CAD system is being done with
mathematicians from the Programming Research Group at Oxford, among
others.
If this is the sort of thing your friend was looking for, I can send more
details. (I'm supposed to be writing a "gosh, wow!" article on all of
this for the popular press...)
Cheers
Greg Wilson
----------------------------------------------------------------------
It's not what you know, it's what you can.
- Alekhine
----------------------------------------------------------------------