RT DW A1 Lu, Huaixi. T1 Specifications to Enable Formal Verification for Hardware and Protocols