"Back to the Moon: The Verification of a Small Microprocessor's Logic Design"
MIT Instrumentation Labs
NASA Office of Logic Design
September 19, 2007, 10 am to 12 noon
NASA Goddard Space Flight Center
Building 11, Directorate Conference Room
All attendees should complete the registration form below and observe the following dates. On-site NASA personnel should also register to aid in event planning and notification of any logistical changes.
Non-US citizens: Not supported for this meeting.
US citizens: September 12, 2007
Webex access: September 17, 2007
Recording of this meeting will not be permitted. Meeting notes will be distributed via http://klabs.org.
Presentation: Back to the Moon
Paper (presented at 2008 DASC): (.doc) -- (.pdf)
Presentation: Back to the Moon
During the Apollo missions to the Moon in the 1960's and 1970's, a small custom processor called the Apollo Guidance Computer provided all onboard computations for Primary Guidance, Navigation and Control, and was built using a primitive gate array: the only logic elements were three-input NOR gates.
The Lunar Orbiter Laser Altimeter (LOLA) will be launched to the Moon in 2008 as part of the Lunar Reconnaissance Orbiter spacecraft and contains an embedded computer to perform real-time calculations to help control this scientific instrument.
LOLA's central processing unit (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 logic elements being a 4:1 multiplexor and a flip-flop.
The architecture of the CPU is considerably more advanced than the original Intel design, with higher performance being derived from more efficient microcoding with most instructions being executed in a single clock cycle and overlap between sequential instructions. Other considerations for this modern CPU include high reliability features such as trapping all unimplemented instructions and halting if a transient error results in executing an unimplemented microcode location.
One task required to certify the LOLA digital electronics is the verification of the custom-designed microprocessor's logic. There are two essential considerations in this task. First, each of the instructions has to do exactly what it is required to do for all combinations of inputs, register and memory assignments, and outputs. Since exhaustive testing of all possible inputs for even this relatively simple computer architecture is not feasible, a combination of systematic and Monte Carlo sampling is used. Second, it has to be verified that the instructions do not inadvertently alter any memory locations, I/O ports, or the state of the processor itself.
Hugh Blair-Smith, one of the original engineers of the Apollo Guidance Computer, took on the task of independently verifying the logic of the LOLA CPU by writing an extensive program that self-tests the system. In this seminar geared toward computer scientists and engineers, Hugh will discuss the fundamental structure of the verification task, give examples of how particular instructions are verified, and review the results of the verification effort to date. Hugh will also include a discussion of several CPU bugs from both the commercial industry and an aerospace flight control system.
The verification program that Hugh designed is being successfully used both in the verification of LOLA CPU's logic as well as in frequency margin testing the LOLA hardware.
Autobiography, August 2007
I was born in New York, but did not remain there long enough to become a Yankee fan, even for a minute. I grew up in Washington, Philadelphia, and Massachusetts; as a pre-teen I took up HO-gauge model railroading and cultivated a fascination with design. In my senior year at Harvard I discovered that computers were what I had been looking for the whole time. My first lessons in the subject were taught by Howard Aiken, so I can claim a sort of "apostolic succession" in the field.
More consequential was falling under the influence of Al Hopkins, Ray Alonso, and others that took the gospel according to Harvard down the river to MIT, but I didn't follow them deliberately. Instead, a moonlighting gig led to an offer from the head of the Digital Computing Group at MIT’s Instrumentation Lab, and I embarked on a 22-year career there, starting with an assignment to write a cross-assembler system for "an unknown number of computers with unknown characteristics," the so-called Mars computers under development by Eldon Hall, Al, Ray, etc. I quickly learned that the art of microprogramming they were developing for these power-frugal machines was even more fun than regular programming. Having spent much spare time in computer company showrooms scrounging programming manuals, I was positioned also to design instruction sets. These activities led to my proudest trophy, a Certificate of Commendation from MIT for "…contribution to computer design and programming for the Apollo Primary Guidance, Navigation and Control System."
Once the pressure of Apollo eased off, somebody advised me to get a life; being a tad inaccurate of hearing even then, I got married. I also got a sailboat, which has maintained my sanity (such as it is). My role in the Space Shuttle program centered around fault tolerance, especially the software-driven synchronization of the spacecraft’s General Purpose Computers. After that was mostly settled, I felt that the government was no longer interested in having a bunch of MIT "scientists" (a cuss word in the mouths of some ungrateful NASA types) push the envelope of computer design, so I plunged into the world of uncertain start-ups. I was on the founding group of Interactive Images (later Easel), and the same again of International Treasury Systems. When that collapsed, I became a migrant worker (software division), which included a brief reprise at what had become Easel before it too collapsed. I finally fetched up at Programart (now absorbed into Compuware), finding there another Apollo colleague, Bob Morse. I enjoyed working both the PC and mainframe sides of this Performance Management house and finally realized that a more sensible fellow would have retired, so I did. Happily, the good folks at the NASA Office of Logic Design realized that I didn't have that much sense, and that I'd have much more fun working from home, getting back to the Moon by verifying an embedded CPU design.
Home - NASA Office of Logic Design
Last Revised: February 03, 2010
Web Grunt: Richard Katz