NASA SBIR 2011 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 11-1 A1.20-8922
SUBTOPIC TITLE: Verification and Validation of Flight-Critical Systems
PROPOSAL TITLE: Scalable Parallel Algorithms for Formal Verification of Software

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Aries Design Automation, LLC
2705 W Byron St
Chicago, IL 60618 - 3745
(773) 856-6633

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav Velev
miroslav.velev@aries-da.com
2705 W Byron St
Chicago, IL 60618 - 3745
(773) 856-6633

Estimated Technology Readiness Level (TRL) at beginning and end of contract:
Begin: 3
End: 4

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
We will develop a prototype of a GPU-based parallel Binary Decision Diagram (BDD) software package. 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 graphics processors (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 a BDD package, and to explore hybrid approaches that will combine this GPU-based BDD package with our GPU-based parallel SAT solver that we are currently developing in a NASA SBIR Phase II project. The goal will be to achieve increased speed, as well as scalability for much larger state spaces when formally verifying complex software for space applications. We anticipate increase in both speed and scalability by 1 – 2 orders of magnitude by the end of Phase I, and 3 – 4 orders of magnitude by the end of Phase II, compared to the current approaches.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The proposed project will result in increase of both speed and capacity when formally verifying complex software. The techniques will also be applicable when formally verifying hardware, proving the correctness of radiation-hardening transformations for digital circuits, mapping of software for execution on reconfigurable architectures such as FPGAs, logic synthesis, power and timing analysis of circuits, scheduling, planning, and solving of constraint optimization problems.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The non-NASA customers will have the same benefits from the technology as NASA. The commercialization will target the major semiconductor, software, and Electronic Design Automation (EDA) companies, as well as NASA prime contractors, aerospace and weapons manufacturers, and all companies that develop embedded systems.

TECHNOLOGY TAXONOMY MAPPING (NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.)
Circuits (including ICs; for specific applications, see e.g., Communications, Networking & Signal Transport; Control & Monitoring, Sensors)
Development Environments
Manufacturing Methods
Models & Simulations (see also Testing & Evaluation)
Quality/Reliability
Robotics (see also Control & Monitoring; Sensors)
Simulation & Modeling
Software Tools (Analysis, Design)
Support
Verification/Validation Tools


Form Generated on 11-22-11 13:43