Systems and methods for automatic formal metastability fault analysis in an electronic design

A system for a formal verification of an electronic design comprising:

• a computing device configured to receive, using at least one processor, a clock-domain crossing electronic design, the at least one processor further configured to analyze the electronic design and automatically generate a set of nodes where metastability can be originated, the at least one processor further configured to automatically generate one or more preconditions representative of metastability effects at the output of at least one synchronizer associated with the electronic design, the at least one processor further configured to automatically generate, based upon, at least in part, the one or more preconditions, one or more properties configured to analyze a propagation of the metastability effects associated with the at least one synchronizer, wherein analyzing the propagation of the metastability effects includes analyzing a fan-out cone associated with the at least one synchronizer, the at least one processor further configured to visually display the metastability effects and one or more unaffected areas at an annotated graph configured to display the at least one synchronizer and at least one clock domain.