  Hamilton-Jacobi reachability analysis is a powerful technique used to verify
the safety of autonomous systems. This method is very good at handling
non-linear system dynamics with disturbances and flexible set representations.
A drawback to this approach is that it suffers from the curse of
dimensionality, which prevents real-time deployment on safety-critical systems.
In this paper, we show that a customized hardware design on a Field
Programmable Gate Array (FPGA) could accelerate 4D grid-based Hamilton-Jacobi
(HJ) reachability analysis up to 16 times compared to an optimized
implementation and 142 times compared to MATLAB ToolboxLS on a 16-thread CPU.
Our design can overcome the complex data access pattern while taking advantage
of the parallel nature of the HJ PDE computation. Because of this, we are able
to achieve real-time formal verification with a 4D car model by re-solving the
HJ PDE at a frequency of 5Hz on the FPGA as the environment changes. The
latency of our computation is deterministic, which is crucial for
safetycritical systems. Our approach presented here can be applied to different
systems dynamics, and moreover, potentially leveraged for higher dimensions
systems. We also demonstrate obstacle avoidance with a robot car in a changing
environment.
