OneSpin Launches "App" for Formal Verification of Floating-Point Hardware Critical for Machine Learning and Deep Learning Chips
November 27, 2018
Blog
Offers Exhaustive Coverage of Floating-Point Arithmetic Operations Compliant with IEEE 754 Standard
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-soluti[...]
