Formal Verification Ensures The Perseverance Rover Lands Safely On Mars

By Joe Hupcey III and Kevin Campbell

Safely landing a spacecraft anywhere on Mars is a complex, high-risk challenge. Even worse, the most scientifically interesting areas of the planet are guarded by boulders, ditches, and tall cliffs — land formations that aren’t very welcoming to vehicles. Such was the case with the Mars Perseverance Rover’s Landing Site: Jezero Crater. It’s not an easy place to find a clear spot to land, but once on-the-ground the potential payoff — finding evidence of ancient microbial life — is profound.(1)

Among the many systems on-board the Perseverance lander needed to support a safe, fully autonomous landing in this hostile area is the Terrain Relative Navigation (TRN) system.(2) In a nutshell, the TRN is a navigation system that operated in the final phases of the lander’s decent to the surface. 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.

Overview of the Terrain Relative Navigation (TRN) system in operation.(3)

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[7]. The processor also interfaces to the spacecraft to obtain the spacecraft state to initialize the TRN.(3)

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, from Siemens EDA, the JPL FPGA designers added synchronization logic to prevent the propagation of metastable events.(4)

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.

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. 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 and remote 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.

References:

(1) Perseverance Rover’s Landing Site: Jezero Crater
https://mars.nasa.gov/mars2020/mission/science/landing-site/

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

(3) 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

(4) 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/

(5) 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/

(6) 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)

Kevin Campbell is a technical product manager at Siemens EDA.