Title: Toward a Formal Verification of a Floating-Point Coprocessor and Its Composition with a Central Processing Unit