Re: Verified compilers?

[Bill Findlay <yaldnif.w@blueyonder.co.uk>]

On 09/03/2012 13:56, in article jjd26i$k12$1@dont-email.me, "Brian Drummond"
<brian@shapes.demon.co.uk> wrote:

> On Thu, 08 Mar 2012 23:38:39 +0000, Bill Findlay wrote:
> 
>> On 08/03/2012 10:23, in article jja1b4$8q1$1@dont-email.me, "Brian
>> Drummond" <brian@shapes.demon.co.uk> wrote:
>> 
>>> On Thu, 08 Mar 2012 10:04:04 +0100, Jacob Sparre Andersen wrote:
>>> 
>>> 
>>>> Oh.  And who verifies that the silicon is correct?
>>> 
>>> VIPER.
>>> 
>>> en.wikipedia.org/wiki/VIPER_microprocessor
>>> www.cl.cam.ac.uk/techreports/UCAM-CL-TR-104.pdf
>> 
>> Was the 'proof' of VIPER not later shown to have missed serious faults?
> 
> Quem vedisti pastores?
> 
> That must be the "controversy" hinted at on Viper's Wikipedia page.
> Unfortunately, apart from the Dick Pountain article in Byte, I don't know
> anything about the VIPER, so any further info would be appreciated.

Sorry - I'm as vague on this as Wikipedia .  I dimly remember some such
thing being discovered years after the 'proof' was ballyhooed.
 
> One area, directly germane to the question above, is that there is a lot
> of commonality between the SPARK subset of Ada, and the synthesisable
> subset of VHDL, probably because both share the need for static
> elaboration of resources. I would like to see this exploited in several
> ways, whether as SystemAda (surely a better alternative to SystemC) for
> SW/HW co-verification or ESL design, or as SPARK-like proof tools applied
> to VHDL.

Interesting point.

-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;