NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal verification of a microcoded VIPER microprocessor using HOLThe Royal Signals and Radar Establishment (RSRE) and members of the Hardware Verification Group at Cambridge University conducted a joint effort to prove the correspondence between the electronic block model and the top level specification of Viper. Unfortunately, the proof became too complex and unmanageable within the given time and funding constraints, and is thus incomplete as of the date of this report. This report describes an independent attempt to use the HOL (Cambridge Higher Order Logic) mechanical verifier to verify Viper. Deriving from recent results in hardware verification research at UC Davis, the approach has been to redesign the electronic block model to make it microcoded and to structure the proof in a series of decreasingly abstract interpreter levels, the lowest being the electronic block level. The highest level is the RSRE Viper instruction set. Owing to the new approach and some results on the proof of generic interpreters as applied to simple microprocessors, this attempt required an effort approximately an order of magnitude less than the previous one.
Document ID
19930011854
Document Type
Contractor Report (CR)
Authors
Levitt, Karl (California Univ. Davis., United States)
Arora, Tejkumar (California Univ. Davis., United States)
Leung, Tony (California Univ. Davis., United States)
Kalvala, Sara (California Univ. Davis., United States)
Schubert, E. Thomas (California Univ. Davis., United States)
Windley, Philip (California Univ. Davis., United States)
Heckman, Mark (California Univ. Davis., United States)
Cohen, Gerald C. (Boeing Aerospace Co. Seattle, WA, United States)
Date Acquired
September 6, 2013
Publication Date
February 1, 1993
Subject Category
COMPUTER SYSTEMS
Report/Patent Number
NASA-CR-4489
NAS 1.26:4489
Funding Number(s)
CONTRACT_GRANT: NAS1-18586
PROJECT: RTOP 505-64-10-07
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Available Downloads

NameType 19930011854.pdf STI