skip to main content
10.1145/1228784.1228869acmconferencesArticle/Chapter ViewAbstractPublication PagesglsvlsiConference Proceedingsconference-collections
Article

A synchronization algorithm for local temporal refinements in perfectly synchronous models with nested feedback loops

Published: 11 March 2007 Publication History

Abstract

Due to the abstract and simple computation and communication mechanism in the synchronous computational model it is easy to simulate synchronous systems and to apply formal verification methods. In synchronous models, a local temporal refinement that increases the delay in a single computation block may affect the functionality of the entire model. To preserve the system's functionality after temporal refinements we provide a synchronization algorithm that applies also to models with nested feedback loops. The algorithm adds pure delay elements to the model in order to balance the delay caused by refinement and to assure concurrent data arrival at computation blocks. It is done so that the refined model stays latency equivalent to the original model. The advantages of our approach are that (a) we remain fully within the synchronous model of computation, (b) we preserve the functionality of the existing computation blocks, and (c) we do not require additional computation resources, wrapper circuits or schedulers.

References

[1]
S. Abdi and D. Gajski. Automatic generation of equivalent architecture model from functional specification. In Proceedings of the Design Automation Conference, pages 608--613, 2004.]]
[2]
A. Benveniste, B. Caillaud, and P. L. Guernic. From synchrony to asynchrony. In Proceedings of the International Conference on Concurrency Theory, pages 162--177, 1999.]]
[3]
G. Berry, M. Kishinevsky, and S. Singh. System level design and verification using a synchronous language. In Proceedings of the International Conference on Computer-Aided Design (ICCAD), page 433, Washington, DC, USA, 2003. IEEE Computer Society.]]
[4]
T. Callahan and J. Wawrzynek. Adapting software pipelining for reconfigurable computing. In Proceedings of the International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES), San Jose, CA, 2000. ACM.]]
[5]
L. Carloni, K. McMillan, and A. SangiovanniVincentelli. Theory of latency-insensitive design. IEEE Transactions on Computer-Aided Design, 20(9), 2001.]]
[6]
L. P. Carloni and A. L. Sangiovanni-Vincentelli. A framework for modeling the distributed deployment of synchronous designs. Formal Methods in System Design, 28(2):93--110, 2006.]]
[7]
S. Edwards, L. Lavagno, E. A. Lee, and A. Sangiovanni-Vincentelli. Design of embedded systems: Formal models, validation, and synthesis. Proceedings of the IEEE, 85(3):366--390, March 1997.]]
[8]
N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. Software Engineering, 18(9):785--793, 1992.]]
[9]
S. Huang, K. Cheng, and K. Chen. On verifying the correctness of retimed circuits. In Proceedings of the the Great Lakes Symposium on VLSI, 1996.]]
[10]
K. Keutzer, S. Malik, A. R. Newton, J. M. Rabaey, and A. Sangiovanni-Vincentelli. System-level design: Orthogonalization of concerns and platform-based design. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 19(12):1523--1543, December 2000.]]
[11]
C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1):5--35, 1991.]]
[12]
N. Maheshwari and S. S. Sapatnekar. Minimum area retiming with equivalent initial states. In Proceedings of the International Conference on Computer-Aided Design, pages 216--219, 1997.]]
[13]
S. Nadjm-Tehrani and J.-E. Strömberg. Formal verification of dynamic properties in an aerospace application. Formal Methods in System Design, 14(2):135--169, March 1999.]]
[14]
D. Potop-Butucaru and B. Caillaud. Correct-by-construction asynchronous implementation of modular synchronous specifications. In Proceedings of the International Conference on Application of Concurrency to System Design, St Malo, France, 2005.]]
[15]
M. Weinhardt and W. Luk. Pipeline vectorization. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, pages 234--248, Feb 2001.]]

Cited By

View all
  • (2008)Application and Verification of Local Nonsemantic-Preserving Transformations in System DesignIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2008.92324927:6(1091-1103)Online publication date: 1-Jun-2008
  • (2007)Synchronization after design refinements with sensitive delay elementsProceedings of the 5th IEEE/ACM international conference on Hardware/software codesign and system synthesis10.1145/1289816.1289826(21-26)Online publication date: 30-Sep-2007

Index Terms

  1. A synchronization algorithm for local temporal refinements in perfectly synchronous models with nested feedback loops

        Recommendations

        Comments

        Information & Contributors

        Information

        Published In

        cover image ACM Conferences
        GLSVLSI '07: Proceedings of the 17th ACM Great Lakes symposium on VLSI
        March 2007
        626 pages
        ISBN:9781595936059
        DOI:10.1145/1228784
        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Sponsors

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        Published: 11 March 2007

        Permissions

        Request permissions for this article.

        Check for updates

        Author Tags

        1. design refinement
        2. synchronization
        3. system design

        Qualifiers

        • Article

        Conference

        GLSVLSI07
        Sponsor:
        GLSVLSI07: Great Lakes Symposium on VLSI 2007
        March 11 - 13, 2007
        Stresa-Lago Maggiore, Italy

        Acceptance Rates

        Overall Acceptance Rate 312 of 1,156 submissions, 27%

        Upcoming Conference

        GLSVLSI '25
        Great Lakes Symposium on VLSI 2025
        June 30 - July 2, 2025
        New Orleans , LA , USA

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • Downloads (Last 12 months)2
        • Downloads (Last 6 weeks)2
        Reflects downloads up to 27 Jan 2025

        Other Metrics

        Citations

        Cited By

        View all
        • (2008)Application and Verification of Local Nonsemantic-Preserving Transformations in System DesignIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2008.92324927:6(1091-1103)Online publication date: 1-Jun-2008
        • (2007)Synchronization after design refinements with sensitive delay elementsProceedings of the 5th IEEE/ACM international conference on Hardware/software codesign and system synthesis10.1145/1289816.1289826(21-26)Online publication date: 30-Sep-2007

        View Options

        Login options

        View options

        PDF

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        Figures

        Tables

        Media

        Share

        Share

        Share this Publication link

        Share on social media