Check equivalence of states by generating a test for a "stuck-at 0" fault at the output
Though this is the "satisfiability problem", unlike using BDDs, process is usually not memory limited
Hardware Verification - Application of formal techniques to chip designs Jacob Abraham (July 7, 2001)