Sequential Synthesis Using S1S
Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto Luigi Sangiovanni-Vincentelli · 1995
In this paper we propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this will lead to simple, rigorous, and constructive solutions for a number of problems arising in the synthesis and optimization of synchronous digital hardware. Specifically, we derive a logical expression which yields a single finite state automaton characterizing the set of implementations which can replace a component in a compositional design. In general the complexity of this automaton is high; we discuss tractable cases, and also determine approximations to the complete set of permissible behavior. We derive procedures which avoid the possible introduction of combinational cycles in optimized designs. We extend our results to designs possessing nondeterminism and fairness. Control aspects of sequential synthesis are also described; specifically, controller realizability is related to classical work on program synthesis and tree automa...