VIPER is the first commercially available microprocessor whose design is claimed to have been proven correct. The controversy provoked by the claim reveals fundamental disagreement about the meaning of 'proof'.

PRODUCTION work should begin next week on the first 32-bit chip in the world with a design that has been proved mathematically to be correct. ... The RSRE's scientists have designed a new software language to work alongside the Viper chips. The language, called NewSpeak, does not allow a programmer to design a program that has errors in it ... And why is it called NewSpeak? It was designed in 1984.

Last month, a small computer consultancy in Worcester went the way of
many others in the current recession, and called in the liquidators.
But the closure of Charter Technologies is not just another hard-luck story:
it contains tough lessons for any company contemplating doing business with
the Ministry of Defence.

Repetitive arrays of cells are much more amenable to CAD than random logic networks, leading to a more highly automated and probably more predictable design process. A custom chip starts from scratch in accumulating reliability statistics, whereas a chip based on a widely used standard substrate can benefit from the experience of other devices. VIPER has therefore been based from the start on gate array and cell array technology. The first VIPER implementation used the UK5000 gate array. This was a joint project between RSRE, Marconi Electronic Devices Ltd (MEDL), British Telecom, and a number of other UK electronics companies. "5000" refers to the number of "usable" gates on the device, allowing for the inevitably less than perfect efficiency of the layout process. The chip actually contains 410 dedicated single-bit latch circuits and 2400 general purpose gate cells, each made up of two N-channel and two P-channel MOSFET's. The latch cells are internally clocked, and are permanently connected together in a serial "scan path" register so that all of them are accessible for testing. The manufacturing technology of UK5000 is silicon gate CMOS, [2 microns]. Layout of a UK5000 chip is fully automatic, once a gate-level description exists. The CAD software is interfaced to the logic design language ELLA, so that a design can be taken automatically from a gate-level description in ELLA through to the final silicon.
VIPERS have been fabricated by MEDL on UK5000 substrates, and (as a private venture) using the CELLSOS Silicon-on-Sapphire process... A third implementation is in progress at Ferranti Electronics Ltd using their proprietary CDI (bipolar) process, which offers good environmental performance with reasonably low cost. All three families of VIPER chips are pin-compatible.The VIPER design is just practical on UK5000, with a bare minimum of "frills". Several highly desirable features have had to be left out of the prototype design... [multiplication, division, a bigger register set, support for redundant parallel VIPERs, DRAM support]