NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Report on the formal specification and partial verification of the VIPER microprocessorThe VIPER microprocessor chip is partitioned into four levels of abstractions. At the highest level, VIPER is described with decreasingly abstract sets of functions in LCF-LSM. At the lowest level are the gate-level models in proprietary CAD languages. The block-level and gate-level specifications are also given in the ELLA simulation language. Among VIPER's deficiencies are the fact that there is no notion of external events in the top-level specification, and it is impossible to use the top-level specifications to prove abstract properties of programs running on VIPER computers. There is no complete proof that the gate-level specifications implement the top-level specifications. Cohn's proof that the major-state machine correctly implements the top-level specifications has no formal connection with any of the other proof attempts. None of the latter address resetting the machine, memory timeout, forced error, or single step modes.
Document ID
19910056502
Acquisition Source
Legacy CDMS
Document Type
Conference Paper
Authors
Brock, Bishop
(Computational Logic, Inc. Austin, TX, United States)
Hunt, Warren A., Jr.
(Computational Logic, Inc. Austin, TX, United States)
Date Acquired
August 15, 2013
Publication Date
June 1, 1991
Subject Category
Computer Operations And Hardware
Accession Number
91A41125
Funding Number(s)
CONTRACT_GRANT: ARPA ORDER 584155
Distribution Limits
Public
Copyright
Other

Available Downloads

There are no available downloads for this record.
No Preview Available