The tool flow and formal verification methods that we will develop will allow NASA to easily retarget the formal verification to any RTOS and user processes, represented as binary code, and to any new processor architecture, given formal definitions of its instruction semantics, memory system, bus, and devices on the bus. By reusing the formal definitions of all functional units for integer, logical, and floating-point instructions in the PowerPC 750 architecture that we have already defined in our NASA SBIR Phase II project titled Efficient Techniques for Formal Verification of PowerPC 750 Executables, it will be possible to formally specify the bit-level semantics of a new processor architecture in several months. Also, we will be able to use the formal definition of the bit-level instruction semantics of the architecture as a non-pipelined specification when formally verifying a new pipelined/superscalar/VLIW implementation processor for that architecture by applying our industrial tool flow for formal verification of pipelined processors. Thus, we will prove that the designs of new processors will implement the exact bit-level specification of the instruction semantics that is used to formally verify the correctness of the software and its interaction with the RTOS, the memory system, bus, and devices on the bus, including under scenarios such as multitasking, interrupt handling, user and kernel mode switching. These capabilities are critical for aerospace applications.
The NASA applications will also benefit other government agencies, such as DoD, DoE, NIST, and NIH. Furthermore, all companies that either manufacture microprocessors or develop IP of microprocessors, as well as all their clients that develop safety-critical software, will be potential users of the resulting technology. As embedded microprocessors are increasingly used in safety-critical applications, many of them controlled by an RTOS, it will become the norm to formally verify the executables for such applications, as the correctness of a microprocessor alone will not be sufficient to guarantee correct execution of the software, and the absence of errors in the binary code will become a requirement. Additional applications will include the formal verification of executables for absence of security vulnerabilities.
More »