OneSpinSolutions 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.”