Description: We will develop an efficient Graphics Processing Unit (GPU) based parallel Binary Decision Diagram (BDD) software package, and will also combine it with our GPU-based parallel SAT solver that we are currently developing in a NASA SBIR Phase II project in order to solve much larger and more complex Boolean formulas from formal verification than possible with either method alone. BDDs are a data structure that satisfies some simple restrictions, resulting in a unique representation of a Boolean function regardless of its actual implementation. This property of BDDs allows the efficient solution of many problems. The proposed tool will exploit multi-core CPUs and the thousands of stream cores in the latest GPUs, which were made accessible to programmers through specialized software development kits. These large numbers of stream cores in GPUs, and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. In the last 8 years, GPUs had an increasing performance advantage of an order of magnitude relative to x86 CPUs. Furthermore, this performance advantage will continue to increase in the next 20 years because of the scalability of the chip manufacturing processes. The technical objectives will be to efficiently exploit the GPU parallelism in order to accelerate the execution of our prototype GPU-based parallel BDD package, and to implement hybrid approaches combining it with our GPU-based parallel SAT solver. BDDs and SAT solvers are orthogonal methods with different advantages, and a hybrid of the two will significantly increase both the speed and capacity when formally verifying complex software for space missions. We achieved at least 2 orders of magnitude speedup with our prototype GPU-based parallel BDD package in a previous Phase I, and expect to achieve at least 4 orders of magnitude speedup with our hybrid BDD-SAT tool by the end of Phase II, compared to the current state of the art.

Benefits: Efficiently solving of challenging Boolean formulas is critical to NASA, as this will increase both the speed and scalability of the following applications: 1) formal verification and testing methods for complex mission software and hardware, including those of the Multi-Purpose Crew Vehicle (MPCV), the next generations of Mars Rovers, and other spacecraft; 2) formal methods to prove the correctness of radiation-hardening transformations for software and hardware; 3) logic synthesis of circuits; 4) Boolean methods for scheduling, planning, and solving of other Constraint Satisfaction Problems (CSPs); 5) formal methods for network coding that will increase both the bandwidth and reliability of space communications by using the existing communication equipment that is already deployed in space after updating the firmware; 6) reliability analysis of hardware, software, and mechanical systems; 7) power and timing analysis of circuits; 8) design of experiments; 9) design of error-correction codes; 10) technology mapping and routing for FPGAs and other reconfigurable circuits; 11) formal methods for cryptanalysis; and 12) cyber security---detecting security vulnerabilities and malicious intent in software.

The potential non-NASA commercial applications include: 1) Formal verification and testing of software and hardware, where the potential customers will be all major semiconductor and software companies. 2) Scheduling, planning, and solving of Constraint Satisfaction Problems (CSPs), where the potential customers will be all companies that use scheduling and planning tools. 3) Solving of Electronic Design Automation (EDA) problems, such as FPGA technology mapping and routing, power and timing analysis of circuits, and formal methods to check the robustness of radiation-hardened circuits, where the potential customers will be all EDA and semiconductor companies. 4) Formal methods for cryptanalysis, where the potential customers will be the Department of Defense, the NSA, and all companies that use cryptanalysis. 5) Formal methods for cyber security, such as for detection of security vulnerabilities and malicious intent in software, where the potential customers will be all companies that develop robust virus scanners based on formal methods, and companies that develop formal methods for detecting security vulnerabilities in software. Because of the potential for a very wide range of software obfuscations that can be used to hide malicious intent, future virus scanners will have to employ efficient formal methods to detect malware, and thus the importance of speed and scalability that will be possible with an efficient hybrid BDD-SAT tool.