Ada Core Nvidia

Joining forces to meet the toughest
safety and security demands.

AdaCore is partnering with NVIDIA™ to implement Ada and SPARK programming languages for select safety-critical firmware used in their next-generation embedded systems platforms. Customer using products such as NVIDIA® Jetson™ for embedded artificial intelligence (AI) computing, NVIDIA DRIVE™ AGX for autonomous vehicle (AV) development, and Isaac™ for Robotics are able to use the same technology at the application level. At the core of NVIDIA’s embedded systems is a system on a chip (SoC) that integrates an ARM architecture central processing unit (CPU), graphics processing unit (GPU), memory controller and IO paths onto one package. AdaCore’s GNAT Pro Ada and SPARK compilers can compile code targeting the ARM CPU embedded on NVIDIA SoCs, and increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262. Supported compilation modes include bare metal as well as Linux or QNX OSes.

NVIDIA's Journey to Adopting SPARK

In this webinar Vice President of software security at NVIDIA, Daniel Rohrer, and Principal Software Engineer Dhawal Kumar talk about the business and technical case for adopting SPARK at NVIDIA. Moderated by Patrick Mannion.

The Ada programming language and its SPARK subset are emerging as compelling alternatives to C for many industries.

Generates Code that is Formally Verified to be Free of Vulnerabilities

The Ada programming language and its SPARK subset combined with its toolset is a platform that allows developers to formally guarantee properties of source code, such as the 100% absence of certain categories of vulnerabilities (buffer overflow, division by zero, references to uninitialized variables, memory corruption), and to prove custom functional assertions.

Increases Critical Code Performance

SPARK and Ada provide performance levels and footprints similar to other system-level languages such as C. However, SPARK allows the removal of proven checks from the final binary, reducing the need for defensive code and allowing for safer and more efficient code execution.

Reduces Development Costs

The demand for cost-effective tools and methodologies has greatly increased in the automotive and industrial domains over the past few years. Using Ada and SPARK reduces the cost of developing safety and security-critical software by automating many verifications that would otherwise need to be done through manual code reviews or testing. It also allows the detection of potential issues early in the development process, reducing the amount of errors needing to be fixed in later stages. For industries that have strong safety, reliability, and security standards, like aerospace and automotive, these benefits can translate to nearly 40 percent cost and time savings from enhanced software verification, according to a study by VDC Research.

Vdc Research Chart

Integrates Easily with Existing C Code

SPARK Ada provides advanced language interfacing capabilities, in particular with C and C++. C and C++ header files can be converted to Ada header files and vice versa. Calls between the two languages can be made directly without any intermediate layer, linked in the same binary with no performance penalty. This allows the progressive introduction of a new language into existing codebases and processes. In addition, the GNAT Pro Common Code Generator (CCG) allows projects to cross-compile Ada and SPARK applications to any hardware target that provides a C compiler, including targets that do not come with off-the-shelf Ada support.

IEC 61508 and ISO 26262 Qualified

Developers need higher integrity software to increase verification efficiencies and achieve compliance with the functional safety standard ISO-26262. The SPARK and Ada compiler, as well as the corresponding formal verification tool, have been qualified at the highest level of ISO 262626 (TCL-3) as well as IEC 61508 (T-3 for the compiler and T-2 for the verification tool). All three products have also been certified by TÜV SÜD, an independent, globally recognized organization that confirms that products meet national and international standards. This qualification enables these tools to be used in the most critical environment in industrial and automotive domains and demonstrates our commitment to support industrial projects on their own path to adoption.

The TÜV SÜD certification mark is widely acknowledged and respected as a trusted symbol of quality, safety, and sustainability.

Tuv Sud Functional S

Future support GPU development with SPARK/Ada on NVIDIA® CUDA®

Available as a beta in Q4 2020, SPARK Ada on NVIDIA® CUDA® will allow formally proven code to be run on an NVIDIA GPU. Contact us and be amongst the first users of the technology!

Contact us about your application

Fill out the form below to request a call with us.