More Web Proxy on the site http://driver.im/

Article

Free access

Sequential synthesis using S1S

Authors:

Felice Balarin,

Robert Brayton,

Alberto Sangiovanni-VincentelliAuthors Info & Claims

ICCAD '95: Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design

Pages 612 - 617

Published: 01 December 1995 Publication History

PDF eReader Publisher Site

Abstract

We present a mathematical framework for analyzing the synthesis of interacting finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in sequential synthesis. We obtain exact and approximate sets of permissible FSM network behavior, and address the issue of FSM realizability. This approach is also applied to synthesizing systems with fairness and timed systems.

References

[1]

J.-K. Rho, G. Hachtel, and F. Somenzi, "Don't Care Sequences and the Optimization of Interacting Finite State Machines," in Proc. Intl. Conf. on Computer-Aided Design, pp. 418-421, Nov. 1991.

[2]

S. Devadas, " Optimizing Interacting Finite State Machines Using Sequential Don't Cares," IEEE Trans. Computer-AidedDesign, pp. 1473-1484, Dec. 1991.

[3]

J. Kim and M. M. Newborne," The Simplification of Sequential Machines With Input Restrictions," IRE Transactions on Electronic Computers, pp. 1440-1443, Dec. 1972.

[4]

H.-Y. Wang and R. K. Brayton, "Input Don't Care Sequences in FSM Networks," in P1vc. Intl. Conf. on Computer-Aided Design, 1993.

Digital Library

[5]

H.-Y. Wang and R. K. Brayton, "Permissible Observability Relations in FSM Networks," in Proc. of the Design Automation Conf., June 1994.

Digital Library

[6]

Y. Watanabe and R. K. Brayton, "The Maximum Set of Permissible Behaviors for FSM Networks," in P1vc. Intl. Conf. on Computer-Aided Design, 1993.

Digital Library

[7]

J. Fron, J. C.-Y. Yang, M. Damiani, and G. D. Micheli, "A Synthesis Framework Based on Trace and Automata Theory," in Workshop Notes of Intl. Workshop on Logic Synthesis, (Tahoe City, CA), May 1993.

[8]

H. Wong-Toi and D. L. Dill, "Synthesizing Processes and Schedulers from Temporal Specifications," in P~vc. of the Second Workshop on Computer-Aided Verification, 1990.

Digital Library

[9]

Z. Manna and R Wolper, "Synthesis of Communicating Processes from Temporal Logic Specifications," ACM Trans. P~vgramming Languagesand Systems, vol. 6, no. 1, pp. 68-93, 1984.

Digital Library

[10]

E. M. Clarke and E. A. Emerson, "Design and Synthesis of Synchronization Skeletons Using Branching Time Logic," in P1vc. Workshop on Logic of Plygrams, vol. 131 of Lecture Notes in Computer Science, pp. 52-71, Springer- Verlag, 1981.

Digital Library

[11]

A. Pnueli and R. Rosner, "On the Synthesis of a Reactive Module," in P~vc. ACM Symposium on Principles of P1vgramming Languages, pp. 179-190,1989.

Digital Library

[12]

W. Thomas, "Automata on Infinite Objects," in Fo~al Models and Semantics (J. van Leeuwen, ed.), vol. B of Handbook of Theoretical Computer Science, pp. 133-191, Elsevier Science, 1990.

Digital Library

[13]

J. E. Hopcroft and J. D. Ullman, Int~vduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.

Digital Library

[14]

J. R. Burch, D. L. Dill, E. Wolf, and G. D. Micheli, "Modeling Hierarchical Combinational Circuits," in P~vc. Intl. Conf. on Computer-Aided Design, pp. 612-617, Nov. 1993.

Digital Library

[15]

J. R. Buchi, " On a Decision Method in Restricted Second Order Arithmetic," in International Congress on Logic, Methodology, and Philosophy of Science, pp. 1-11,1960.

[16]

A. Aziz, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Synthesizing Interacting Finite State Machines," Tech. Rep. UCB/ERL M94/96, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, Dec. 1994.

[17]

K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[18]

E.A. Emerson, "Temporal and Modal Logic," in Fo1~al Models and Semantics (J. van Leeuwen, ed.), vol. B of Handbook of Theoretical Computer Science, pp. 996-1072, Elsevier Science, 1990.

Digital Library

[19]

S. Safra, "Exponential Determinization for ~o-Automata with Strong-Fairness Acceptance Condition," in P~vc. ACM Symposium on the Theory of Computing, 1992.

Digital Library

[20]

R. Alur and D. L. Dill, "Automata for Modelling Real Time Systems," in International Colloquium on Automata, Languages and Programming, 1990.

Digital Library

[21]

R. Alur, L. Fix, and T. Henzinger, "A Determinizable Class of Timed Automata," in P1vc. of the Computer Aided Verification Conf., 1994.

Digital Library

Cited By

Katis AGacek AWhalen M(2016)Towards synthesis from assume-guarantee contracts involving infinite theoriesProceedings of the 4th FME Workshop on Formal Methods in Software Engineering10.1145/2897667.2897675(36-41)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2897667.2897675
Winkelmann K(2001)Formal Methods in Designing Embedded Systems—the SACRES ExperienceFormal Methods in System Design10.1023/A:101129593136719:1(81-110)Online publication date: 1-Jul-2001
https://dl.acm.org/doi/10.1023/A%3A1011295931367
Park SChoi K(1999)Performance-driven scheduling with bit-level chainingProceedings of the 36th annual ACM/IEEE Design Automation Conference10.1145/309847.309932(286-291)Online publication date: 1-Jun-1999
https://dl.acm.org/doi/10.1145/309847.309932
Show More Cited By

Index Terms

Sequential synthesis using S1S
1. Hardware
  1. Integrated circuits
    1. Logic circuits
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

A transformation from PPTL to S1S
COCOA'10: Proceedings of the 4th international conference on Combinatorial optimization and applications - Volume Part II

A transformation from Propositional Projection Temporal Logic (PPTL) as well as Propositional Interval Temporal Logic (PITL) with infinite models to monadic second order logic with one successor (S1S) is presented in this paper. To this end, intervals ...
Sequential synthesis using S1S

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 ...
Acceleration of Test Generation for Sequential Circuits Using Knowledge Obtained from Synthesis for Testability

In this paper, we propose a method of accelerating test generation for sequential circuits by using the knowledge about the availability of state justification sequences, the bound on the length of state distinguishing sequences, differentiation between ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '95: Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design

December 1995

748 pages

ISBN:0818672137

Chairman:
Richard Rudell
Synopsys, Inc., Mountain View, CA

Copyright © Copyright (c) 1995 Institute of Electrical and Electronics Engineers, Inc. All rights reserved.

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS: Computer Society

Publisher

IEEE Computer Society

United States

Publication History

Published: 01 December 1995

Check for updates

Author Tags

Qualifiers

Article

Conference

ICCAD '95

Sponsor:

SIGDA
IEEE-CS

ICCAD '95: International Conference on Computer Aided Design

November 5 - 9, 1995

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
161
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)1

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Katis AGacek AWhalen M(2016)Towards synthesis from assume-guarantee contracts involving infinite theoriesProceedings of the 4th FME Workshop on Formal Methods in Software Engineering10.1145/2897667.2897675(36-41)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2897667.2897675
Winkelmann K(2001)Formal Methods in Designing Embedded Systems—the SACRES ExperienceFormal Methods in System Design10.1023/A:101129593136719:1(81-110)Online publication date: 1-Jul-2001
https://dl.acm.org/doi/10.1023/A%3A1011295931367
Park SChoi K(1999)Performance-driven scheduling with bit-level chainingProceedings of the 36th annual ACM/IEEE Design Automation Conference10.1145/309847.309932(286-291)Online publication date: 1-Jun-1999
https://dl.acm.org/doi/10.1145/309847.309932
Khatri SNarayan AKrisnan SMcMillan KBrayton RSangiovanni-Vincentelli APennino TYoffa E(1996)Engineering change in a non-deterministic FSM settingProceedings of the 33rd annual Design Automation Conference10.1145/240518.240604(451-456)Online publication date: 1-Jun-1996
https://dl.acm.org/doi/10.1145/240518.240604
Wang HBrayton RRudell R(1995)Multi-level logic optimization of FSM networksProceedings of the 1995 IEEE/ACM international conference on Computer-aided design10.5555/224841.225156(728-735)Online publication date: 1-Dec-1995
https://dl.acm.org/doi/10.5555/224841.225156

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents