In this SBIR Phase I project, we will design and formally verify a fault-tolerant processor core implementing the RISC-V Instruction Set Architecture (ISA), augmented with arrays of reconfigurable processing elements and possibly other mechanisms to accelerate image and science data processing. The proposed work will achieve fault tolerance, high performance, high reliability, and low power consumption in a very agile architecture that can be reconfigured dynamically for optimal or near optimal performance for many applications. Also, by using processor cores implementing the free open-source RISC-V ISA, NASA will benefit from the constant stream of innovations in the extremely active R&D field of this architecture, which is being vigorously developed by tens of companies and hundreds of researchers worldwide.
We have made critical contributions to formal verification of complex microprocessors. We will apply our extremely efficient tool flow for formal verification of pipelined/superscalar/VLIW processors that outperforms other approaches by orders of magnitude, while requiring minimal manual intervention, and scales for mathematically proving of both safety and liveness for a wide range of microprocessor architectures with many architectural mechanisms. Another application of our tool flow is the formal verification of correctness and cybersecurity properties of executable code for a given ISA with a formally defined specification.
The need for formal verification of digital avionics for aerospace applications cannot be overemphasized after the Boeing 737 MAX crisis, with its high cost in lost human lives (346 people died in the two fatal crashes), and economic damage to both the manufacturer (more than $18.6B loss for Boeing, not including potential future economic losses from damaged reputation), and its customers (billions of dollars loss for the airlines that had purchased airplanes from this model that had to be grounded for more than 1.5 years).
The proposed processor will accelerate many applications at NASA, such as image and science data processing, e.g., signal/sensor processing, AI methods, and edge computing, including astrophysics, planet weather modeling, etc. Compared to other designs, it will have higher reliability and lower power consumption, allowing much faster solutions of problems that can be solved with current processors, and enabling solutions of larger problems. NASA can use this processor in spacecraft, satellites, rovers, robots, spacesuits, and embedded devices.
The proposed work will similarly benefit all aerospace, defense, engineering, pharmaceutical, e-commerce, financial, and other companies that require fault-tolerant image and science data processing, as well as those developing medical devices, equipment for nuclear power stations, automotive, and other safety-critical applications. We will commercialize both physical chips and IP processor cores.