Efficient Techniques for Formal Verification of PowerPC 750 Executables

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$600,000.00
Award Year:
2009
Program:
SBIR
Phase:
Phase II
Contract:
NNX09CA19C
Award Id:
87954
Agency Tracking Number:
075477
Solicitation Year:
2007
Solicitation Topic Code:
X1.02
Solicitation Number:
n/a
Small Business Information
IL, Chicago, IL, 60660-5818
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
361627933
Principal Investigator:
MiroslavVelev
Principal Investigator
(773) 856-6633
miroslav.velev@aries-da.com
Business Contact:
MiroslavVelev
Business Official
(773) 856-6633
miroslav.velev@aries-da.com
Research Institute:
n/a
Abstract
We will develop an efficient tool for formal verification of PowerPC 750 executables. The PowerPC 750 architecture is used in the radiation-hardened RAD750 flight-control computers that are utilized in many space missions. The resulting tool will be capable of formally checking: 1) the equivalence of two instruction sequences; and 2) properties of a given instruction sequence. The tool will automatically introduce symbolic state for state variables that are not initialized and for external inputs. We bring a tremendous expertise in formal verification of complex microprocessors, formal definition of instruction semantics, and efficient translation of formulas from formal verification to Boolean Satisfiability (SAT). We will also produce formally verified definitions of the PowerPC 750 instructions used in the project, expressed in synthesizable Verilog; these definitions could be utilized for formal verification and testing of PowerPC 750 compatible processors, for FPGA-based emulation of PowerPC 750 executables, as well as in other formal verification tools to be implemented in the future.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government