Modeling and optimization of hierarchical synchronous circuits

Synchronous designs are often described and implemented hierarchically as a network of interacting finite state machines. When the individual components are synthesized and implemented separately, it is desirable to take into account the degrees of freedom that arise from the interactions with the other components and from the specification. Specifically, we consider the problem of finding the complete set of implementations that can be correctly substituted for a component in a system without changing the behavior of the total system. In this paper, a synchronous trace set model is proposed to tackle this problem. The unambiguous way in which this model describes synchronous behavior provides us with a general method to model interacting finite state machines. We show that a single synchronous trace set can be used to characterize all possible substitutions in a correct substitution problem. We give a necessary notion of progress that permits us to choose a correct one from this set, or to show that no solution exists. We provide results of an implicit implementation of our approach applied to benchmarks ranging from small to very large state machines. These results show the feasibility of the proposed methods