Actions for Report on the formal specification and partial verification of the VIPER microprocessor

Email RIS file
Bookmark
Report an Issue

Report on the formal specification and partial verification of the VIPER microprocessor

Author
Hunt, Warren A., Jr.
Published
Jul 1, 1991.
Physical Description
1 electronic document
Additional Creators
Brock, Bishop
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
The formal specification and partial verification of the VIPER microprocessor is reviewed. The VIPER microprocessor was designed by RSRE, Malvern, England, for safety critical computing applications (e.g., aircraft, reactor control, medical instruments, armaments). The VIPER was carefully specified and partially verified in an attempt to provide a microprocessor with completely predictable operating characteristics. The specification of VIPER is divided into several levels of abstraction, from a gate-level description up to an instruction execution model. Although the consistency between certain levels was demonstrated with mechanically-assisted mathematical proof, the formal verification of VIPER was never completed.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 19910018472.
Accession ID: 91N27786.
NASA-CR-187540.
NAS 1.26:187540.
Terms of Use and Reproduction
No Copyright.
View MARC record | catkey: 15680050