Generating Correctly Rounded Math Libraries for New Floating Point Variants
summary
Generates polynomials that approximate the correctly rounded value (not the real value) and encodes coefficient constraints as an LP-formulated constraints system solved by an LP solver; uses MPFR 2000-bit oracle to get exact rounded targets and a generator called rLibm generator to build native math libraries. Produces correctly rounded results for all inputs for Bfloat16 and Posit16 elementary functions, exposes a double-rounding bug in repurposed libs (millions of wrong cases), and yields CPU speedups of ~1.3–2.0× versus repurposed float/double libs.
AI-written summary · about
chapters (9)
- 0:00Start
- 1:40Important Requirements for Math Libraries
- 1:59Math Libraries Should Be Efficient
- 4:41Minimax Approximation Method
- 5:46Range Reduction
- 11:38Special Case Inputs
- 12:43Rounding Interval
- 17:28Generate a Polynomial Approximation
- 24:41Conclusion
related talks
22mOne Polynomial Approximation to Produce Correctly Rounded Results of an Elementa
22mCorrectly Rounded Math Libraries without Worrying about the Application’s Rounding Mode
58mPortable floating-point calculations
58mFrom Formal Verification to Correctly Rounded Math Libraries
10mCorrectly Rounded Dot Products under Round-to-Odd
14mFPL: Fast Presburger Arithmetic through Transprecision
11mPrinting floating point numbers is surprisingly hard!!
23mGenerating Programs for Polynomial Multiplication with Correctness Assurance