The non-NASA commercialization will target companies that would need to quickly develop processor cores 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 tool to automatically generate a symbolic simulator from the formal definition of the instruction semantics of the ISA, allowing them to formally verify properties of the executables for the new processors---we are currently developing this technology in an ongoing NASA SBIR Phase 2 project entitled Efficient Techniques for Formal Verification of PowerPC 750 Executables. 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 semiconductor companies that we have established contacts with. The resulting technology will allow NASA to very quickly design and formally verify radiation-hardened, reconfigurable VLIW processors that are binary-code compatible with a given legacy Instruction Set Architecture (ISA) that has a formal definition of its instruction semantics, such that the processors can be custom-tailored to accelerate specific space applications. Furthermore, it will be possible to add reconfigurable functional units and new instructions, and to formally verify the resulting processor for binary-code compatibility with the legacy ISA. We will have several competitive advantages: 1) we will be able to reuse the formal definitions of the instruction semantics of the PowerPC 750 ISA that we are currently developing for an ongoing NASA SBIR Phase 2 project; 2) we will be able to use our industrial-strength tool flow for design and formal verification of pipelined/superscalar/VLIW processors, and prove both safety and liveness with it; 3) we will combine this tool flow with our parallel GPU-based SAT solver that is up to 2 orders of magnitude faster than the best publicly available sequential SAT solvers, and was developed in a recent NASA SBIR Phase 1 project; and 4) we will be able to provide a tool to automatically generate a symbolic simulator from the formal definition of the instruction semantics of the ISA, allowing the users to formally verify properties of the executables for the new processors.
More »