Synthesizable System Verilog model for hardware metastability in formal verification

In this work, we present a formal analysis method that incorporates a standard hardware and property description language, System Verilog, and information from clock domains analysis to detect circuits that do not tolerate hardware metastability effect. We provide a case study to prove the feasibility and usefulness of the approach.