Pro Tip: Planning to Land Your Spacecraft on Mars? You Will Need CDC, RDC, and Formal Property Checking

If you are an engineer at one of the growing number of entities looking to land a spacecraft on Mars (SpaceX, ESA, Bradbury), you already know that your spacecraft’s success must rely on a completely self-contained, completely reliable, on-board navigation system to guide your craft safely to touchdown. The pros at the Jet Propulsion Laboratory (JPL) have done this many times, so naturally their example merits careful study.

Among the many systems that their most recent lander needed to support a safe, fully autonomous landing on the red planet is the Terrain Relative Navigation (TRN) system(1). In a nutshell, as Perseverance approached the target landing site, the TRN compared the stored images of the surrounding landscape against real-time images taken by a high-resolution camera on the bottom of the lander. If the stored images and the live feed from the camera “overlapped”, the spacecraft was on the right track and the craft continued its flight per its pre-programmed trajectory. Conversely, if there was any misalignment between the stored and live images, the TRN’s processor would have directed the landing retrorocket system to steer the craft back on a safe course.

Developed in 2018 by engineers at Jet Propulsion Laboratory (JPL) in Pasadena, CA, the core electronics of the TRN is comprised of the following:

An Inertial Measurement Unit (IMU) and camera are interfaced to a dedicated compute element composed of a general-purpose flight processor (PowerPC) and a field programmable gate array (FPGA). The FPGA times the sensor data and performs highly parallel image processing algorithms. The flight processor coordinates the data flow, eliminates any spurious landmark matches, and estimates the vehicle state. The processor also interfaces to the spacecraft to obtain the spacecraft state to initialize the TRN.(2)

Formal clock domain crossing verification is essential to make sure that the clock signals in the FPGA will not become unsynchronized over time, and thus “hang” the chip. To elaborate, today’s FPGA designs include multiple cores, interfaces, test logic, and even different internal power and voltage domains. In particular, the multiple asynchronous clocks, and the signals crossing between asynchronous clock domains, may result in functional errors. Specifically, when a signal from one asynchronous clock domain is sampled by a register on a different asynchronous clock domain, the setup/hold timing requirement will be violated for the destination register. This setup/hold timing violation means that the destination register will probably become metastable, so the destination register will settle to an unpredictable value and cause a functional error. To address this, with guidance from the Questa CDC tool, the JPL FPGA designers added synchronization logic to prevent the propagation of metastable events.(3)

Adding to this challenge is the overlay of reset signaling. In the past, verifying a design’s reset signaling was a pretty straightforward process — simply confirm the continuity of the reset signal from the pad ring to all the IP blocks and instances inside a design under test. But with the TRN’s sophisticated logic design, there is a risk that previously unknown bugs could arise from the aggressive optimization of reset signaling networks required to reduce power and area overhead. Bugs can also be introduced by putting together IP blocks that handle clocking and reset differently. The JPL engineers used Questa RDC to leverage the CDC path and waiver information taken from Questa CDC analysis, then execute a comprehensive, automated, formal-based analysis that focused on the actual functional reset-domain crossing paths to achieve the highest throughput and most deterministic path to actionable results.(4)

Because even the most well written constrained-random simulation testbenches cannot traverse every part of a design’s state space, the JPL team used the Questa PropCheck tool to complement their digital simulations of the TRN design.(5) Formal analysis with property checking explores the whole state space in a breadth-first manner, versus the depth-first approach used in simulation. Property checking is, therefore, able to exhaustively discover any design errors that can occur, without needing specific stimulus to detect the bugs. This ensures that the verified design is bug-free in all legal input scenarios. At the same time, this approach inherently identifies unreachable coverage points, which helps accelerate coverage closure.

With such a complex landing procedure, getting the design right was the only option. Formal analysis with CDC, RDC, and property checking provided the JPL team the tools they needed to mitigate risk and successfully land the Perseverance Rover on Mars. Hence, if you are looking to develop equally sophisticated (and successful) flight hardware, you will likely need to adopt these technologies and methodologies as well.

Happy landings to your Mars program!

Joe Hupcey III,
for the Siemens EDA Verification Team

References:

(1) High-level article:
Terrain Relative Navigation: Landing Between the Hazards
https://science.nasa.gov/technology/technology-highlights/terrain-relative-navigation-landing-between-the-hazards

(2) Much more detailed technical paper on the TRN system:
Real-Time Terrain Relative Navigation Test Results from a Relevant Environment for Mars Landing, Andrew E. Johnson, Yang Cheng, James Montgomery, Nikolas Trawny, Brent Tweddle, and Jason Zheng, Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA 91109
https://trs.jpl.nasa.gov/bitstream/handle/2014/45631/14-5083_A1b.pdf?sequence=1

(3) More background on CDC verification for FPGA designs:
Significantly Improve Your FPGA Design Reliability by Using Custom CDC Synchronizers
https://blogs.sw.siemens.com/verificationhorizons/2018/04/24/significantly-improve-your-fpga-design-reliability-by-using-custom-cdc-synchronizers/

(4) More background on Reset Domain Crossing (RDC) verification:
How to Avoid Metastability on Reset Signal Networks, a/k/a Reset Check is the New CDC
https://blogs.sw.siemens.com/verificationhorizons/2016/07/21/how-to-avoid-metastability-on-reset-signal-networks-aka-reset-check-is-the-new-cdc/

(5) Technical paper on a prior application of Questa Formal verification to a JPL project:
Using Formal to Exhaustively Determine Unsafe Clock Ratios Between Asynchronous Blocks, Eric Hendrickson, JPL — https://trs.jpl.nasa.gov/handle/2014/46428
(Also presented at DVCon USA 2018)