Reconfigurable VLIW Processor for Software Defined Radio

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.

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.

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.

This is early/mid-stage (TRL 6) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.