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
Document Type
Contractor Report (CR)
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
Report/Patent Number
NAS 1.26:4489
Funding Number(s)
PROJECT: RTOP 505-64-10-07
Distribution Limits
Work of the US Gov. Public Use Permitted.

Available Downloads

NameType 19930011854.pdf STI