USA flag logo/image

An Official Website of the United States Government

Efficient Techniques for Formal Verification of PowerPC 750 Executables

Award Information

Agency:
National Aeronautics and Space Administration
Branch:
N/A
Award ID:
87954
Program Year/Program:
2009 / SBIR
Agency Tracking Number:
075477
Solicitation Year:
N/A
Solicitation Topic Code:
N/A
Solicitation Number:
N/A
Small Business Information
Aries Design Automation, LLC
2705 West Byron Street Chicago, IL 60618-3745
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 2
Fiscal Year: 2009
Title: Efficient Techniques for Formal Verification of PowerPC 750 Executables
Agency: NASA
Contract: NNX09CA19C
Award Amount: $600,000.00
 

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.

Principal Investigator:

Miroslav N. Velev
Principal Investigator
7738566633
miroslav.velev@aries-da.com

Business Contact:

Miroslav N. Velev
Business Official
7738566633
miroslav.velev@aries-da.com
Small Business Information at Submission:

Aries Design Automation, LLC
6157 N Sheridan Road, Suite 16M Chicago, IL 60660

EIN/Tax ID: 202887585
DUNS: N/A
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No