NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Report on the formal specification and partial verification of the VIPER microprocessorThe 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.
Document ID
19910018472
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Brock, Bishop (Computational Logic, Inc. Austin, TX, United States)
Hunt, Warren A., Jr. (Computational Logic, Inc. Austin, TX, United States)
Date Acquired
September 6, 2013
Publication Date
July 1, 1991
Subject Category
Computer Programming And Software
Report/Patent Number
NASA-CR-187540
NAS 1.26:187540
Accession Number
91N27786
Funding Number(s)
CONTRACT_GRANT: ARPA ORDER 58-4155
CONTRACT_GRANT: NASA ORDER L-39627C
PROJECT: RTOP 505-66-21
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available