Achieving End-to-End Formal Verification of Large Floating-Point Dot Product Accumulate Systolic Designs