Design and Formal Verification of a RISC-V DSP for Space Communication

In this SBIR Direct to Phase II project, we will design and formally verify a reconfigurable pipelined Digital Signal Processor (DSP) that will implement the free open-source RISC-V Instruction Set Architecture (ISA), and will be optimized for next-generation modems and routers for space communication. The free open-source RISC-V ISA will allow the Air Force to benefit from the constant stream of innovation in the extremely active research field of this architecture, for which R&D is done by hundreds of scientists and tens of companies worldwide. The resulting reconfigurable pipelined DSP for space communication will have many applications of interest to the Air Force, Space Force, and all other DOD branches. The proposed work will benefit from 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: branch prediction, exceptions, multicycle functional units, advanced and speculative loads, predicated execution, register remapping, out-of-order execution based on a reorder buffer, delayed branches, data-value prediction, mechanisms to correct soft errors by re-executing affected instructions, reconfigurable functional units, arrays of reconfigurable processing elements, multi-threaded execution, and reconfigurable polymorphic heterogeneous multi-core architectures. 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 computer hardware and software 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 so far, 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 1.5 years so far). The cost of critical failures of weapons systems due to bugs in their computers could be even greater, including compromised U.S. national security. The anticipated technical result is a formally verified reconfigurable pipelined DSP that implements the free open-source RISC-V ISA, and is optimized for next-generation modems and routers for space communication. That this DSP design will be formally verified will be crucial for all safety-critical applications, including weapons systems.