Sequential synthesis using S1S
- 1 October 2000
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
- Vol. 19 (10) , 1149-1162
- https://doi.org/10.1109/43.875301
Abstract
We propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant solutions to 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 that can replace a component of a larger design. The power of our approach is demonstrated by the fact that it generalizes immediately to arbitrary interconnection topologies, and to designs containing nondeterminism and fairness. We also describe control aspects of sequential synthesis and relate controller realizability to classical work on program synthesis and tree automata.Keywords
This publication has 21 references indexed in Scilit:
- The maximum set of permissible behaviors for FSM networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Input don't care sequences in FSM networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A synthesis framework based on trace and automata theoryPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Exact and heuristic algorithms for the minimization of incompletely specified state machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Permissible observability relations in FSM networksPublished by Association for Computing Machinery (ACM) ,1994
- A fully implicit algorithm for exact state minimizationPublished by Association for Computing Machinery (ACM) ,1994
- Model construction for implicit specifications in modal logicPublished by Springer Nature ,1993
- Automata on Infinite ObjectsPublished by Elsevier ,1990
- On the Supremal Controllable Sublanguage of a Given LanguageSIAM Journal on Control and Optimization, 1987
- The Simplification of Sequential Machines with Input RestrictionsIEEE Transactions on Computers, 1972