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 poser. In this paper we extend the notion of series-parallel posers to allow the modeling of systems involving global iteration. For this class of systems we present a verification algorithm, and discuss its foundation.