OneSpin Launches “App” for Formal Verification of Floating-Point Hardware Critical for Machine Learning and Deep Learning Chips

November 26 16:00 2018 Print This Article

Offers Exhaustive Coverage of Floating-Point Arithmetic Operations Compliant with IEEE 754 Standard

MUNICH, Germany and SAN JOSE, Calif., Nov. 27, 2018 (GLOBE NEWSWIRE) — OneSpin® Solutions today launched OneSpin 360 DV Floating Point Unit (FPU) App, an application add-on to the OneSpin 360 DV Property Checker™ for the formal verification of floating-point hardware compliant with the IEEE 754 standard. 

The new app offers exhaustive coverage to uncover deep, corner-case bugs in IEEE 754 implementations and includes a reliable model of floating-point arithmetic operations optimized for formal analysis, increasing development speed and quality of IEEE 754 FPUs. It verifies that results of arithmetic operations accurately match the standard’s specifications, checking all rounding modes and exception flags. Half, single or double precision formats can be selected, less common precisions can be accommodated, and users can selectively disable checks. All major operations are supported except division.

Integration with the OneSpin 360 verification platform lets engineers use all 360 DV advanced debug features. Additional dedicated debug capabilities are available, including a high-level view of floating-point data types to accelerate the analysis and debug process. Complexity issues are mitigated through the automatic selection of OneSpin’s proof engines and strategies.

“Machine learning and deep learning place high demands on performance and accuracy of FPUs,” remarks Nicolae Tusinschi, product specialist, design verification at OneSpin. “This app enables engineers to uncover deep, corner-case bugs with minimal effort and gain full confidence in their IEEE 754 implementations. The FPU App found bugs on multiple verified production designs, a testament to its exhaustive coverage of floating-point arithmetic operations.”

Floating Point Units in Chips

Most artificial intelligence (AI) chips that power machine learning (ML) and deep learning (DL) applications include FPUs. Algorithms used in neural networks often use multiplication and addition of floating-point values. In particular, convolutional neural networks (CNNs), popular for computer vision applications, may involve deeply nested loops of floating-point operations, which subsequently need to be scaled to different sizes in order to meet the precision and area requirements.

These applications have elevated the value of FPUs in contemporary chips and increased the importance of thorough design verification of floating-point hardware. For example, even an apparently minor bug in an implementation causing a small rounding mistake can have a huge impact as errors accumulate over many operations. In addition, the IEEE 754 floating-point standard defines many corner-case scenarios and non-ordinary values, such as +0, -0, signed infinity and NaN (not a number). Four rounding modes and five exception flags are possible as well. This complexity is hard to capture manually when setting up a simulation or formal verification environment, making an off-the-shelf automated solution attractive.

Xilinx Use of OneSpin FPU App

As detailed in a 2018 Design and Verification Conference (DVCon) paper, Xilinx used the OneSpin FPU App to verify a floating-point design. Real-world results showed how scalability and performance arose from the automation and the ability of formal analysis to prove complex assertions.

Slides are available at https://bit.ly/2INqq43 and a paper can be found at https://bit.ly/2CAAUnl.

The OneSpin app also found multiple bugs in the fpu100 IP from OpenCores and these were reported back to the developers.

Availability and Pricing

The OneSpin 360 DV FPU App is shipping now.

Pricing is available upon request. OneSpin has direct sales channels in the United States, Europe and throughout Asia, backed by a variety of customer service and support options including on-site training, hotline support and consulting services.

To learn more about the OneSpin’s FPU App, visit https://www.onespin.com/fpu/.

About OneSpin Solutions

OneSpin Solutions has emerged as a leader in formal verification through a range of advanced electronic design automation (EDA) solutions for digital integrated circuits. Headquartered in Munich, Germany, OneSpin enables users to address design challenges in areas where reliability really counts: safety-critical verification, SystemC/C++ high-level synthesis (HLS) code analysis and FPGA equivalence checking. OneSpin’s advanced formal verification platform and dedication to getting it right the first time have fueled dramatic growth over the past five years as the company forges partnerships with leading electronics suppliers to pursue design perfection. OneSpin: Making Electronics Reliable.

Engage with OneSpin at:
Website: www.OneSpin.com
Twitter: @OneSpinSolution
LinkedIn: https://www.linkedin.com/company/onespin-solutions
Facebook: https://www.facebook.com/OneSpinSolutions

OneSpin, OneSpin Solutions and the OneSpin logo are trademarks of OneSpin Solutions GmbH. All other trademarks are the property of their respective owners.

For more information, contact:

Nanette Collins                         
Public Relations for OneSpin
(617) 437-1822                                                  
[email protected]

  Categories:
view more articles

About Article Author

Jonathan Yaniv
Jonathan Yaniv

Jonathan is the founder and editor-in-chief of TrustedNerd.com. Covering major tech shows such as CES, Jonathan is always there for the latest tech news. Want your gadget to be reviewed or have a release you'd like to be considered for publishing? Send Jonathan an email, jonathan [at] trustednerd.com

View More Articles
0 comments