Formal Methods for Robustness Checking of Radiation-Hardened-by-Design Microelectronics

For more than four decades, space-based systems have been used to support the detection of activities associated with the proliferation of weapons of mass destruction. This project will develop efficient and scalable tool to evaluate the robustness of radiation-hardened circuits and to automatically generate recommendations for radiation hardening in these space systems. The tool will be based on efficient translation of the problem to Boolean Satisfiability (SAT), in order to exploit the recent advances in both the speed and capacity of SAT solvers. Relative to previous formal approaches for robustness checking, Phase I will achieve a capability to analyze circuits that are at least an order-of-magnitude larger in terms of their gate count. An extensive experimental evaluation will be conducted in Phase II. Commercial Applications and other Benefits as described by the awardee In addition to DOE applications, a highly scalable tool for automatic analysis of the robustness of radiation hardened circuits should benefit all branches of the DoD and NASA, all semiconductor companies, and companies that develop aerospace electronics