1. A method of verifying a design for at least a portion of a logic system, the method comprising: deriving a state transition graph (STG) for the design; recursively decomposing the STG to determine all non-trivial strongly connected components of the STG; and comparing an infinite behavior represented by each strongly connected component to an expected behavior of the design to validate the design.