Equivalence Checking of a Floating-Point Unit Against a High-Level C Model