Formal verification of globally-iterated and locally-non-iterated finite state machines

Formal verification of hardware has significantly gained in popularity as an alternative to testing and simulation in hardware design. Recently we introduced a new methodology for verification of non-iterated systems. The technique is based on the inductively defined notion of a series-parallel poset. In this paper we extend the notion of series-parallel posets to allow the modeling of systems involving global iteration. For this class of systems we present a verification algorithm, and discuss its foundation