NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Toward a formal verification of a floating-point coprocessor and its composition with a central processing unitDiscussed here is work to formally specify and verify a floating point coprocessor based on the MC68881. The HOL verification system developed at Cambridge University was used. The coprocessor consists of two independent units: the bus interface unit used to communicate with the cpu and the arithmetic processing unit used to perform the actual calculation. Reasoning about the interaction and synchronization among processes using higher order logic is demonstrated.
Document ID
19910019463
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Pan, Jing (California Univ. Davis., United States)
Levitt, Karl N. (California Univ. Davis., United States)
Cohen, Gerald C. (Boeing Military Airplane Development Seattle, WA, United States)
Date Acquired
September 6, 2013
Publication Date
August 5, 1991
Subject Category
Computer Systems
Report/Patent Number
NASA-CR-187547
NAS 1.26:187547
Accession Number
91N28777
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.

Related Records

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