A fundamental manifestation of the system-level nature of the modern SOC has been in the explosion of untimed paths on a chip. A single chip is no longer a textbook synchronous entity. Thanks to the use of complex design methodologies like asynchronous clock domains, interacting dynamic power domains, aggressive dynamic reset schemes, the wide-spread use of timing exceptions, GALS design practices etc., large swaths of a chip behave like asynchronous circuits. The analysis of such behavior is outside the sweet-spot of logic simulation + STA that the design community been riding for the last two and a half decades. Naturally, associated chip failures are being encountered in increased numbers and have acquired an insidious aura because they are often detected late in the design process with obviously adverse effects on budgets and business models. Fortunately, this urgent problem has also driven rapid innovation in the EDA community leading to a static verification framework comprising of a synthesis of semantic analysis and formal methods that enables sign-off level confidence for failure modes arising from such untimed paths. The success of this new class of EDA tools is evidenced, for example, by the fact that every single SOC today is signed-off using a dedicated clock-domain-crossing verification tool. This is a new paradigm in that these new EDA tools are targeted solutions for critical failure modes, representing a change from the incumbent practice of trying to make generic tools like simulators work for any type of design failure. It is expected that the solution-oriented approach for tackling untimed paths will serve as a template to make inroads into SOC verification complexity arising from other types of failure modes.