floating-point 1 Datapath Verification of Floating-Point Multipliers with Case Splitting Sep 19, 2025