NASA Office of Logic Design

A scientific study of the problems of digital engineering for space flight systems,
with a view to their practical solution.

Verification

"Drilling for Certainty" David Brooks NY Times May 27, 2010	Interesting Op-Ed (Complexity and Human Understanding): Intro -- But the real issue has to do with risk assessment. It has to do with the bloody crossroads where complex technical systems meet human psychology. These systems, which allow us to live as well as we do, are too complex for any single person to understand. Yet every day, individuals are asked to monitor the health of these networks, weigh the risks of a system failure and take appropriate measures to reduce those risks.
"Back to the Moon: The Verification of a Small Microprocessor's Logic Design" Seminar: presented by Hugh Blair-Smith Presentation: Back to the Moon Paper: (.doc) -- (.pdf) 27th Digital Avionics Systems Conference October 26-30, 2008	Abstract The original and primary task of self-test program Smalley3 was independent verification of the logic design of the LOLA DU (Lunar Orbiter Laser Altimeter Digital Unit) microprocessor. Tasks were added to verify continuing correct operation of this central processing unit (CPU) under margin testing for supply voltage, ambient temperature, and clock frequency. Finally, an on-orbit diagnostic task was added so that any malfunctions of LOLA in lunar orbit can be identified as faults in, or not in, the CPU. The Lunar Reconnaissance Orbiter spacecraft will be launched to the Moon in 2009 with six scientific instruments including LOLA, each containing an embedded microprocessor to perform real-time subsystem control calculations. LOLA's CPU is a small, custom-designed processor, designed to meet the mission requirements while minimizing resources. This 8-bit machine is essentially code compatible with Intel's 8085 but is implemented in modern technology, an advanced, radiation-hardened 0.15 µm gate array, with the only logic element types being a 4:1 multiplexor and a flip-flop. This paper explains the fundamental structure of the verification task, shows how particular instructions are verified, presents a high-coverage scheme for detecting inadvertent RAM alteration, describes subsystem testing of RAM, and reviews the results of the verification effort. Some infamous CPU design flaws from both the commercial industry and aerospace flight control systems are discussed.
SAFETY-SPECIFIC ANALYSIS AS ADDITIONAL DESIGN ASSURANCE FOR MICROPROCESSORS Håkan Forsberg, Saab Avitronics, Jönköping, Sweden 27th Digital Avionics Systems Conference October 26-30, 2008	Abstract In this paper we discuss the use of safety-specific analysis (SSA) as additional design assurance of modern microprocessors. SSA is a method to derive and validate safety-specific requirements about internal operations of a component. We suggest and discuss a mixed component assurance approach based on on-chip service history, on-chip architectural mitigation techniques (including turning off some parts) and safety-specific analysis on different parts of the microprocessor. With this approach we believe that it might be possible to gain certification credit for the complete microprocessor even if some on-chip parts are partially or even completely new. We also show why it will be very hard to perform safety-specific analysis on a complete modern microprocessor. A modern microprocessor is simply too complex and manipulates data in a too complex manner to be able to analyze for safety-specific aspects.
Microprocessor Evaluations for Safety-Critical, Real-Time Applications: Authority for Expenditure No. 43 Phase 1 Report DOT/FAA/AR-06/34 Office of Aviation Research and Development December, 2006	Abstract The intent of this report is to provide findings about safety issues in using today’s microprocessors on aircraft. It considers the applicability of RTCA/DO-254 to microprocessors, documents potential safety concerns when using modern microprocessors on aircraft, and proposes potential approaches for addressing these safety concerns. The project is being performed in two phases with participation from avionic system developers (BAE Systems, The Boeing Company, and Smiths Aerospace) and Federal Aviation Administration organizations responsible for aircraft safety research and development. Phase 1 established the project scope and identified the research parameters as documented in this report. This report presents an assessment of existing certification guidelines towards certification of microprocessors. It indicates that new validation processes are required in addition to the existing ones. The report identifies that microprocessor obsolescence management may become a significant problem in the future due to rapidly changing designs. This report also addresses unpredictable issues in computational components of the microprocessors that may lead to safety concerns in avionics applications. The microprocessor testing and evaluation trends are presented, and several safety concerns are identified related to the testing and validation. In the next phase, studies will be made to incorporate a set of recommended guidelines towards selection and qualification of microprocessors in the certification process.
Microprocessor Evaluations for Safety-Critical, Real-Time Applications: Authority for Expenditure No. 43 Phase 2 Report DOT/FAA/AR-08/14 Air Traffic Organization Operations Planning Office of Aviation Research and Development June, 2008	Abstract The intent of this report was to provide findings about safety issues in using today’s microprocessors on aircraft. The research effort considered the applicability of RTCA/DO-254 to microprocessors, documented potential safety concerns when using modern microprocessors on aircraft, and proposed potential approaches for addressing these safety concerns. The project was performed in multiple phases with participation from avionic system developers (BAE Systems, The Boeing Company, Lockheed Martin, and Smiths Aerospace) and Federal Aviation Administration organizations responsible for aircraft safety research and development. Phase 1 established the project scope and identified the research parameters. Phase 1 reviewed the available literature and surveyed microprocessor users to identify the issues and potential solutions associated with the use of microprocessors in regulated safety-critical applications. Phase 2, documented in this report, developed the project objectives and found an approach to work toward the solution of these issues and the achievement of these objectives. Phase 3 is intended to validate this approach and continue the development of processes, services, and prototype tool development. These results will be documented in a Microprocessor Selection and Evaluation Handbook to facilitate application to real-world, safety-critical applications. Current trends toward using commercial off-the-shelf (COTS) microprocessors present safety challenges, especially with growing design complexity, the vast array of supported features, and limited design documentation. A formal framework for the approval of COTS microprocessors in aerospace systems is essential. This report proposes a Microprocessor Approval Framework that is applicable to COTS microprocessors.
Microprocessor Evaluations for Safety-Critical, Real-Time Applications: Authority for Expenditure No. 43 Phase 3 Report DOT/FAA/AR-08/55 Air Traffic Organization Operations Planning Office of Aviation Research and Development February, 2009	Abstract This report discusses the findings concerning safety issues in using today’s commercial off-the-shelf (COTS) microprocessors on aircraft. The report addresses the applicability of RTCA/DO-254 to microprocessors, documents potential safety concerns when using modern COTS microprocessors on aircraft, and proposes potential approaches for addressing these safety concerns. The research was performed in multiple phases with participation from avionic system developers (BAE Systems, The Boeing Company, Lockheed Martin, and Smiths Aerospace) and Federal Aviation Administration organizations responsible for aircraft safety research and development. Phase 1 established the project scope and identified the research parameters, as well as reviewed the available literature and surveyed microprocessor users to identify the issues and potential solutions associated with the use of COTS microprocessors in regulated, safety-critical applications. Phase 2 developed the project objectives and found an approach to work toward the solution of these issues and the achievement of these objectives. Phase 3, documented in this report, evaluated the proposed approach and continued the development of processes, services, and prototype tool development. Phase 4, depending heavily on industry experience, will attempt to determine if new approaches can be developed to ensure system safety and provide more effective methods to accumulate safety evidence for certification while reducing the time and cost to develop and certify complex systems. These results will be documented in a Microprocessor Selection and Evaluation Handbook to facilitate application to real-time, safety-critical applications.
Microprocessor Evaluations for Safety-Critical, Real-Time Applications: Authority for Expenditure No. 43 Phase 4 Report * GET THIS REPORT WHEN IT COMES OUT *
Design Guidelines and Criteria for Space Flight Digital Electronics
Design, Analysis, and Test Guides
Accelerated Verification of Digital Devices Using VHDL^XL Sandi Habinc and Peter Sinander European Space Agency	Abstract This paper presents two aspects for improving the verification of microprocessors; program-less verification, and methods for handling large differences in abstraction level between a reference model and the actual design. Program-less verification is a type of pseudo random verification where the notion of a software program executing on the microprocessor has been abandoned.
Why Engineers Should Consider Formal Methods C. Michael Holloway NASA LaRC 16th Digital Avionics Systems Conference, October 27-30, 1997	Abstract This paper presents a logical analysis of a typical argument favoring the use of formal methods for software development, and suggests an alternative argument that is simpler and stronger than the typical one.
ICASE RQ: Formal Methods for the Quality Assurance of Digital Systems Gerald Lüttgen ICASE Research Quarterly	Introduction (excerpt) Formal Methods is an area of research in Computer Science which aims at improving the reliability and safety of digital systems by applying mathematical specification and verification techniques. It complements traditional approaches to quality assurance such as reviews and testing. The absence of malbehavior is of particular importance for safety-critical systems, such as used in traffic control, medicine, aeronautics, and aerospace. Experience shows that many fatal errors occur very rarely and under exceptional circumstances; one major source being the intrinsic interplay of concurrent processes as well as the inherent complexity of fault-tolerant systems.
Design, Test, and Certification Issues for Complex Integrated Circuits Report No. DOT/FAA/AR 95/31 L. Harrison and B. Landell August 1996	Abstract This report provides an overview of complex integrated circuit technology, focusing particularly upon application specific integrated circuits. This report is intended to assist FAA certification engineers in making safety assessments of new technologies. It examines complex integrated circuit technology, focusing on three fields: design, test, and certification.. It provides the reader with the background and a basic understanding of the fundamentals of these fields. Also included is material on the development environment, including languages and tools. Application specific integrated circuits are widely used in Boeing 777 fly by wire aircraft. Safety issues abound for these integrated circuits when they are used in safety critical applications. Since control laws are now executed in silicon and transmitted from one integrated circuit to another. reliability issues for these integrated circuits take on a new importance. This report identifies certification risks relating to the use of complex integrated circuits in fly by wire applications.
Results for the Programmable Logic Usage and Assurance Surveys Presentation Survey Results plassurance.xls pLusage.xls	Objective: The objective of this research is to first determine where and how Programmable Logic (PL) is used within NASA and document the current methods of assurance. With that information, to perform a gap analysis between NASA practices and industry/military standards and practices. Prepare training material for NASA assurance personnel and engineers on the assurance of PL.
SOFTWARE ASPECTS OF STRATEGIC DEFENSE SYSTEMS Communications of the ACM, December 1985, Volume 28, Number 12. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear. and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise or to republish. requires a fee and/or specific permission.	Note: While some of this paper is specific to the SDI system back in the 1980's, a good amount of the engineering analysis is applicable to those who wish to treat the digital logic design problem as a software task and use software methods. This analysis is applicable to our work today. -- rk Summary: This report comprises eight short papers that were completed while I was a member of the Panel on Computing in Support of Battle Management, convened by the Strategic Defense Initiative Organization (SDIO). Why software is unreliable Why the SDI software system will be untrustworthy Why conventional software development does not produce reliable programs The limits of software engineering methods Artificial intelligence and the Strategic Defense Initiative Can automatic programming solve the SDI software problem? Can program verification make the SDI software reliable? Is SDIO an efficient way to fund worthwhile research?
Verification Guild	Summary: A Community of Verification Professionals
Averant: White Papers	Automatic Verification of Timing Exceptions AMBA Compliance Checking using Static Functional Verification ARM's Paper on X Analysis - Tech Committee Award, SNUG '03 Solidify Verifies Design's Behavior Using Static Functional Verification in the Design of a Memory Controller Role of static methods in HDL verification Introduction to Property Checkers for Functional Verification Accelerating Functional Closure Using Solidify and Hardware Emulation Static Functional Verification with Solidify: A New Low-Risk Methodology for Faster Debug of ASICs and Programmable Parts
Verification Methodology Manual: Techniques for Verifying HDL Designs David Dempster and Michael Stuart © 2001 by Teamwork International and TransEDA Limited	Contents Overview of Front-End Tools Code and Rule Checking in the Design Flow Introduction to Coverage Analysis Coverage Analysis in the Design Flow Practical Value of Coverage Analysis Coverage Analysis Measurements Coverage directed Verification Methodology Verification Architecture for Pre-Silicon Validation Overview of Test Bench Requirements Analyzing and Optimizing the Test Suite

Home - NASA Office of Logic Design
Last Revised: May 29, 2010
Digital Engineering Institute
Web Grunt: Richard Katz