Formal verification ensures Perseverance rover lands safely on Mars

By Joe Hupcey III and Kevin Campbell

Landing a spacecraft safely anywhere on Mars is a complex and high-risk challenge. Worse still, the most scientifically interesting areas of the planet are guarded by rocks, ditches and high cliffs – land formations that are not very welcoming to vehicles. This was the case with the landing site of the Mars Perseverance Rover: Jezero Crater. It’s not an easy place to find an open spot to land, but once in the field, the potential payoff – finding evidence of ancient microbial life – is profound.(1)

Among the many systems aboard the Perseverance lander needed to enable a safe and 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 stages of the lander’s descent to the surface. As Perseverance approached the target landing site, the TRN compared stored images of the surrounding landscape to 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 according to its pre-programmed trajectory. Conversely, if there was a misalignment between the stored and live images, the TRN’s processor would have directed the retrorocket landing system to return the craft to a safe course.

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

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

An inertial measurement unit (IMU) and camera are interfaced to a dedicated computational element consisting of a general purpose flight processor (PowerPC) and a field programmable gate array (FPGA). The FPGA times sensor data and runs highly parallel image processing algorithms. The flight processor coordinates the data stream, eliminates any erroneous waypoint matches and estimates the vehicle’s condition[7]. The processor also interfaces with the spacecraft to obtain the state of the spacecraft to initialize the TRN.(3)

Formal verification of the clock domain crossover is essential to ensure that the clock signals in the FPGA will not become out of sync over time, and therefore “freeze” the chip. To elaborate, today’s FPGA designs include multiple cores, interfaces, test logic, and even different internal power and voltage domains. In particular, multiple asynchronous clocks and signals crossing asynchronous clock domains can lead to functional errors. Specifically, when a signal from one asynchronous clock domain is sampled by a register on a different asynchronous clock domain, the set/hold timing requirement will be violated for the destination register. This setup/hold synchronization violation means that the destination register will likely become metastable, so the destination register will stabilize at an unpredictable value and cause a functional error. To solve this problem, with guidance from Siemens EDA’s Questa CDC tool, JPL FPGA designers added timing logic to prevent the propagation of metastable events.(4)

Added to this challenge is the overlapping of reset signaling. In the past, verifying a design’s reset signaling was a fairly straightforward process – simply confirm the continuity of the pad ring’s reset signal to all blocks and IP instances inside a design being tested. But with the sophisticated logic design of the TRN, there is a risk that previously unknown bugs could result from aggressively optimizing the reset signaling networks needed to reduce zone power and overload. Bugs can also be introduced by assembling IP blocks that handle synchronization and reset differently. JPL engineers used Questa RDC to leverage the CDC path and disclaimer information gained from the Questa CDC analysis, then run a comprehensive, automated, and formal analysis that focused on the actual functional crossing paths of the domain of reset to achieve the highest and most deterministic throughput. path to actionable results.

Since even the best-written constrained random simulation testbeds cannot traverse every part of a design’s state space, the JPL team used the Questa PropCheck tool to complement their numerical simulations of the TRN design. Formal analysis with property checking explores the entire state space breadth-first, compared to the depth-first approach used in simulation. Property verification is therefore able to comprehensively discover all design errors that may occur, without the need for specific stimulus to detect bugs. This ensures that the verified design is bug-free in all legal input scenarios. At the same time, this approach inherently identifies inaccessible coverage points, helping to expedite coverage closure.

With such a complex and remote landing procedure, good design was the only option. The formal analysis with CDC, RDC and Property Verification provided the JPL team with the tools they needed to mitigate risk and successfully land the Perseverance Rover on Mars.

References:

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

(2) Top-level article:
Terrain Navigation: Land Between Obstacles
https://science.nasa.gov/technology/technology-highlights/terrain-relative-navigation-landing-between-the-hazards

(3) Much more detailed technical note on the TRN system:
Real-Time Terrain Relative Navigation Test Results of an Environment Relevant to Landing on Mars, 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 information on CDC verification for FPGA designs:
Dramatically Improve the Reliability of Your FPGA Design 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 information about 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 document on a prior application of Questa formal verification to a JPL project:
Formal use to comprehensively determine dangerous 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 Technical Product Manager at Siemens EDA.

Joseph Hupcey III

Joseph Hupcey III

(All posts)

Joe Hupcey III is part of the Siemens EDA Product Management Team for Design and Verification Technologies; based in Siemens’ office in Silicon Valley, California. He is responsible for the Formal product line of automated applications and advanced property verification. Prior to joining Siemens, Hupcey held product management and marketing positions at several Electronic Design Automation (EDA) companies, for products spanning multiple aspects of hardware and software functional verification. Before moving into marketing, he worked as an electrical engineer in FPGA design, EDA tools for FPGAs and ASICs, and ASIC verification. Joe’s education includes BSEE, MSEE and MBA degrees from Cornell University in Ithaca, NY.