From Informal Specifications to an ABV Framework for Industrial Firmware Verification