NVIDIA is in the process of migrating some product lines to a new architecture using the RISC-V ISA. The company will also upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK. These moves will increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.
Ada and SPARK are designed to help meet the most stringent software requirements for safety and security. The Ada programming language has built-in features that detect code defects early in the software life cyclet. The SPARK language — a restricted set of Ada features designed to perform a formal mathematical proof — increases the certainty of catching defects early that might not have been detected otherwise. SPARK facilitates static analysis that can formally demonstrate certain properties of the code, ranging from correct data flows and the absence of run-time errors such as overflow, to more advanced assertions and satisfaction of functional requirements.