Microcode Verification Project.
Final technical rept.,
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
Pagination or Media Count:
Within the scope of this project, a formalism for representing state transitions in a computationally tractable way has been invented, and a proof system based on this formalism has been designed and implemented. The representations of state transitions are called state deltas. The basic proof system has been specialized for proofs about machine language and microcode by the addition of simplification rules for bitstring arithmetic, and by the addition of a translator from the ISPS machine description language to state deltas. Some experimentation with the system has been driven by a preliminary attempt to verify parts of the microcode of the Fault-Tolerant Spaceborne Computer FTSC. The primary success to date has been the verification of the basic algorithm used for computing floating point square root. Author
- Computer Programming and Software
- Computer Hardware