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.
More »