Temporal decomposition for logic optimization

Traditional approaches for sequential logic optimization include (1) explicit state-based techniques such as state minimization, (2) structural techniques such as retiming, and (3) methods that exploit sequential don´t-cares derived from unreachable states. These approaches optimize a logic circuit as a single component with a single input/output behavior. In this paper we present a novel concept for sequential optimization referred to as temporal decomposition, which distinguishes the logic that initializes the circuit from the logic needed for the behavior after startup. This work was motivated by a recent observation made for bounded property verification: There is a substantial optimization potential for transition relations when the first execution steps are applied as satisfiability don´t-cares. This result suggests that current designs include circuitry that is only used during the first few clock periods after reset and could be discarded or disabled after startup. In this paper we describe how temporal decomposition could be applied to treat the logic for startup separately from the remaining circuitry and discuss multiple alternatives to exploit this for an improved implementation.