For as long as people have used Verilog, dealing with Xs in models has been a problem –
The root of that was wanting a simple signal model that wouldn’t take up much memory in the early Verilog simulators – cache performance being a major determinant of simulation speed, so packing 0,1,X,Z into 2-bits worked well.
However in the early days of Verilog there was usually one power domain and one reset, so Xs were easy to eliminate. The addition of multiple power domains and level-shifting makes that model too simple for modern use, and the problem has spawned a bunch of new tools.
However, those tools are probably not necessary, the real solution is to change the signal model so that Xs don’t get in the way of other verification. As of user-defined nettypes being added to SystemVerilog (a few years ago) you can do that yourself.
The 1/0/X/Z model collapses three orthogonal concepts: value, strength, and certainty into an single value, which means if it’s X, you can’t tell what the value should be to be consistent. If you separate the concerns and do value calculations independently of certainty (and strength) then the logic state can be consistent regardless of certainty. That’s easy enough to do in a user-defined nettype with a bit for each dimension.
So what else can we do with that? Well, you can do type conversions on the dimensions independently – change between using a logic 1/0 for value and a real number (for Voltage), without having to worry about what to do with Xs (handy for analog/digital boundaries). You can use more bits in the certainty dimension – not-set, power missing, timing missed, etc.
Changing the model also lets you verify circuits that you would rather build without resets, e.g. divider chains in PLLs. So you can save yourself the transistors.