NASA SBIR 2009 Solicitation

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Aries Design Automation, LLC
2705 W Byron St
Chicago, IL 60618 - 3745
(773) 856-6633

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav N. Velev
miroslav.velev@aries-da.com
2705 W Byron St
Chicago, IL 60618 - 3745
(773) 773-6633

Estimated Technology Readiness Level (TRL) at beginning and end of contract:
Begin: 5
End: 6

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
We will implement an environment for design, formal verification, compilation of code, and performance and power evaluation of Systems on a Chip (SOCs) consisting of heterogeneous processor cores that can be single-issue pipelined, superscalar, or VLIW, and are binary-code compatible with any existing Instruction Set Architecture (ISA). Particularly, we will ensure binary-code compatibility with the PowerPC 750 ISA, which is used in the radiation-hardened RAD750 flight-control computer that is utilized in many NASA space missions, including Deep Impact, the Mars Reconnaissance Orbiter, the Mars Rovers, and is planned to be used in the Crew Exploration Vehicle (CEV). The processor cores will have reconfigurable functional units and corresponding specialized instructions that can be optimized to accelerate any application. Our focus in this Phase 2 project will be on Software Defined Radio (SDR) applications. The radiation-hardening will be done at the microarchitectural level with a mechanism that will allow the detection and correction of all timing errors---caused not only by radiation, but also by variations in the voltage, frequency, manufacturing process, and aging of the chip. The binary-code compatibility of the processor cores with the PowerPC 750 ISA will allow them to seamlessly execute legacy binary code from previous space missions. We have made critical contributions to the fields of formal verification of complex pipelined microprocessors, and Boolean Satisfiability (SAT), and have developed highly efficient Electronic Design Automation (EDA) tools that we will use.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The project will result in an environment for design and formal verification of SOCs consisting of heterogeneous processor cores that are radiation-hardened, reconfigurable, and binary-code compatible with any legacy ISA. It will be possible to add new instructions that use reconfigurable functional units to accelerate specific applications, such as SDR.

We have several competitive advantages:
1) we will reuse the formal definitions of the instruction semantics of the PowerPC 750 ISA that we are developing in a current NASA SBIR Phase 2 project;
2) we will apply our industrial-strength tool for design and formal verification of pipelined/superscalar/VLIW processors to prove safety, liveness, and binary-code compatibility of the processor cores with the given legacy ISA;
3) our SAT-based techniques for technology mapping of operations to reconfigurable functional units, invented on our own expenses, and up to 8 orders of magnitude faster than previous methods;
4) a tool to automatically generate a symbolic simulator and formal property checker from the formal definitions of instruction semantics of the ISA extended with new instructions, allowing the user to formally verify properties of the executables---a current NASA SBIR Phase 2 project;
5) we will combine the above tools with our GPU-based parallel SAT solver that is at least 2 orders of magnitude faster than the best publicly available solvers, and that we are developing in a current NASA SBIR Phase 2 project.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The non-NASA commercialization will target companies that would need to quickly develop processor cores and SOCs that are radiation-hardened, computationally powerful, reconfigurable, and custom-tailored to specific applications. Our competitive advantage will be due to our technology to easily design pipelined/superscalar/VLIW processors that are binary code compatible with a given ISA that has a formal definition of its semantics, and to automatically formally verify both safety and liveness of those processors. Furthermore, we will be able to provide our customers with a retargetable tool to automatically generate a symbolic simulator and formal property checker from the formal definitions of the instruction semantics of the given ISA, possibly extended with new instructions, allowing the users to formally verify properties of the executables for the new processors---we are developing this tool in a current NASA SBIR Phase 2 project.

After the completion of Phase 2, the immediate customers will be the over 40 member companies of Power.org, an organization whose purpose is to develop, enable, and promote PowerPC architecture technology. We also plan to collaborate with several major companies that we have established contacts with.

The reconfigurable functional units in the processor cores can be used for hardware and software obfuscation to complicate a reverse-engineering effort---of interest to companies that manufacture weapons systems.

TECHNOLOGY TAXONOMY MAPPING (NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.)

Architectures and Networks Autonomous Control and Monitoring Autonomous Reasoning/Artificial Intelligence Computer System Architectures Data Input/Output Devices Highly-Reconfigurable On-Board Computing and Data Management Operations Concepts and Requirements Pilot Support Systems Radiation-Hard/Resistant Electronics Simulation Modeling Environment Software Development Environments Software Tools for Distributed Analysis and Simulation Testing Facilities Testing Requirements and Architectures Ultra-High Density/Low Power