ARIES DESIGN AUTOMATION, LLC — National Aeronautics and Space Administration SBIR Phase I: Z2

Description

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 Ramp;D field of this architecture, which is being vigorously developed by tens of companies and hundreds of researchers worldwide.nbsp;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.nbsp;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).