🚀 go-pugleaf

new@ee.udel.edu (Darren New) writes:
> In article <RNMAX3C@xds13.ferranti.com> peter@ficc.ferranti.com (Peter da Sil
> >                         How do you specify hardware and human actions
> >based on a formal language specification?
> 
> I understand a CPU called "viper" has in some way been formally validated.
> Check out ACM architecture-oriented journals.

This is correct. The Viper CPU is a relatively simple CPU design; it was
necessary to keep it so in order to make it validatable. The formal proof
system for hardware is based around the language ML; you specify the actions
of various elements of the design, and the system uses inference rules to
construct a formal proof that the design is correct (or incorrect :-)

There are still a number of problems with proving hardware correctness. For
example, it is difficult to codify the behaviour of transistors accurately.
Most transistor models either make too many assumptions to be generally
applicable, or are too complicated to be tractable using automated proof
methods.

It is also the case that the proof is only as good as the information put in
at the start. If what you say the hardware is does not match the actual chip
layout, your proof is useless.

In spite of this, formal verification of hardware is useful, and research
continues. If people are interested I could dig out some examples of hardware
verification. I think they are working on Viper II, which will be a slightly
more useful chip (i.e. one which you might actually want to build into
something more complicated than a toaster).

> In any case, a formal semantics for Ada would allow you to know that
> the validation suite tested all parts of the compiler.  These tests
> would not necessarily assure you that the compiler is correct, of course.

The problem is that most powerful and expressive languages have complicated
and messy formal semantics. As soon as you start allowing pointers, goto
statements, side-effects like x = y++ and the like, your semantics become
horribly complicated or even impossible to formulate.

I'm personally unconvinced by denotational semantics; it seems to be a way of
spraying some maths over the problem to make it look like a formal proof of
something, and I can't see that big an advantage over operational semantics.
Still, it wasn't my favourite course by any means, and I may have been
misled.

Certainly operational semantics is useful as a way of expressing what a
particular bit of code does in a much less ambiguous and more tractable way
than is possible via an English-language description.

> BTW, in reference to the FORTH-based NOVA chip:
> I can't find the reference, but that isn't suprising since most of
> my journals are in boxes in another state.  I suspect I read about
> it in one of the ACM publications, probably ASPLOS.  Definitely sometime
> around 1987 or 1988.

It's called the NOVIX.


mathew

--
If you're a John Foxx fan, please mail me!