FPGA Equivalence Checking For A Nuclear Safety Controller

Every chip development team wants to find and fix all the bugs they possibly can in pre-silicon verification. Turning a chip to fix issues found in the bring-up lab incurs high costs and product delays; bugs found in the field are even more expensive to repair. But for some applications, including military/aerospace, implanted medical devices, and autonomous vehicles, the consequences of a faulty chip can be deadly. Electronic systems for nuclear power plants are another clear example of designs with extremely high standards for verification. At OneSpin’s inaugural Osmosis users’ group meeting in Munich, one of our expert users presented a riveting talk on formal equivalence checking for FPGA designs used in nuclear applications.

Jürgen Dennerlein is a product development, I&C hardware development expert and platform architect at Framatome GmbH. He began his talk by introducing Framatome, a 60-year-old company that has provided the equipment for 92 nuclear power plants around the world. They design plants, provide steam supply systems, design and manufacture components and fuel assembles, integrate automation systems, and service all types of nuclear reactors. Jürgen works specifically on instrumentation and control (I&C) for nuclear steam supply systems. He proudly reported that Framatome has installed 82 safety I&C systems in 44 nuclear power plants in 17 countries spanning Europe, Asia, South America, and North America.

The products they create are strongly regulated by standards, particularly IEC 62566 within the IEC SC 45A standard series. While this standard does not dictate the development process, it includes requirements that weigh heavily in the verification flow used by Jürgen’s team. For example, verification activities must be run by staff independent of those performing design and implementation. The standard focuses on post-implementation verification and detection of potentially adverse effects of logic simplifications and gate duplications, and potential faults resulting from the development tools themselves or from their use. Framatome adds another requirement supplemental to the standard: verification activities must be run by tools independent of those used for design and implementation.

One verification approach that fits squarely within the scope of the standard is formal equivalence checking to verify that the post-route netlist of a chip is mathematically equivalent to the original RTL design. Unlike simulation, equivalence checking is exhaustive and requires no test vectors. Jürgen pointed out that systematic errors from logic synthesis or place-and-route tools are difficult to find by netlist simulation based on directed testing since the test vectors might not excite the right corner cases to trigger bugs.

The Framatome I&C designs use FPGAs, which adds more complexity to the flow. FPGA implementation tools offer a wide range of optimizations, many of which significantly alter the state elements in the design. Traditional ASIC-style combinational equivalence checking relies on a direct mapping between the state elements in the RTL and those in the netlist. For FPGAs, sequential equivalence checking is required to handle the changes made by optimizations. Jürgen said they selected OneSpin 360 EC-FPGA for this purpose, noting that is entirely independent of the Intel Quartus Prime FPGA synthesis and place-and-route software.

Jürgen presented a specific example of an Intel Cyclone V FPGA used in the Framatome Compact Safety Controller. He said that the most demanding module in the entire controller system is the processing module and that the heart of this module is a double-precision floating-point unit (FPU). This FPU implements not only the expected addition, subtraction, and multiplication, but also such complex operations as division, square root, and logarithms. Trying to verify the post-route netlist by simulation alone would take “many, many, many” years. Of course, no amount of simulation could ever be exhaustive or provide the certainty of formal equivalence checking. The results of running EC-FPGA to compare the FPU post-synthesis Verilog netlist against the FPU post-place-and-route Verilog netlist included:

• Low initial effort for training and self-study (five working days total)
• Easy and straightforward setup based on a simple template script from OneSpin
• No manual mapping required between the two netlists
• Regression capability due to the automated mapping
• No reduction of RAM within FPU required

The bottom line: EC-FPGA was able to prove the two netlists for this complex design equivalent in a total run time of less than one hour. Jürgen commented that he was pleased with these results and praised the OneSpin Applications Engineering team for their “highly engaged, very responsive support, even on weekends!” We were delighted to hear this news and are very grateful to Jürgen and Framatome for sharing their story with our user community. If you were unable to attend Osmosis yourself, you can watch a video of the presentation. Verification doesn’t get any more critical than for nuclear power plant electronics, so we’re sure you’ll find this talk every bit as compelling as we did.