Accessible formal verification for safety-critical hardware design

Formal verification is a vital aspect of safety-critical system design, not only to ensure proper functionality but also to provide formal proof of that functionality to regulators and oversight committees. However, few hardware engineers are trained in formal techniques, creating a dangerous disconnect between specification/design and verification. This paper presents ongoing work on the development of a technique to make formal verification of hardware designs more accessible to specification and design engineers by creating a library that abstracts the formal domain into a verified set of basic operations and components. Therefore, engineers can specify systems using these operations and components, which are automatically converted into the formal domain by the library for verification and design generation. Existing designs (including intellectual property (IP) blocks) can be verified against specifications following the opposite route. Making the formal domain more accessible to engineers will help integrate design and verification, rather than leaving verification as only a post-design review. While independent verification will always remain important to safety qualification, enabling the people who specify and design hardware systems to also verify them will result in safer and more easily qualified systems.