World Scientific
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
Our website is made possible by displaying certain online content using javascript.
In order to view the full content, please disable your ad blocker or whitelist our website

System Upgrade on Mon, Jun 21st, 2021 at 1am (EDT)

During this period, the E-commerce and registration of new users may not be available for up to 6 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.

POLYCHRONY for System Design

    Rising complexities and performances of integrated circuits and systems, shortening time-to-market demands for electronic equipments, growing installed bases of intellectual property (IP), requirements for adapting existing IP blocks with new services, all stress high-level design as a prominent research topic and call for the development of appropriate methodological solutions. In this aim, system design based on the so-called "synchronous hypothesis" consists of abstracting the nonfunctional implementation details of a system and lets one benefit from a focused reasoning on the logics behind the instants at which the system functionalities should be secured. With this point of view, synchronous design models and languages provide intuitive (ontological) models for integrated circuits. This affinity explains the ease of generating synchronous circuits and verify their functionalities using compilers and related tools that implement this approach. In the relational mathematical model behind the design language SIGNAL, this affinity goes beyond the domain of purely synchronous circuits, and embraces the context of complex architectures consisting of synchronous circuits and desynchronization protocols: globally asynchronous and locally synchronous architectures (GALS). The unique features of the relational model behind SIGNAL are to provide the notion of polychrony: the capability to describe circuits and systems with several clocks; and to support refinement: the ability to assist and support system design from the early stages of requirement specification, to the later stages of synthesis and deployment. The SIGNAL model provides a design methodology that forms a continuum from synchrony to asynchrony, from specification to implementation, from abstraction to concretization, from interfaces to implementations. SIGNAL gives the opportunity to seamlessly model circuits and devices at multiple levels of abstractions, by implementing mechanisms found in many hardware simulators, while reasoning within a simple and formally defined mathematical model. In the same manner, the flexibility inherent to the abstract notion of signal, handled in the synchronous-desynchronized design model of SIGNAL, invites and favors the design of correct by construction systems by means of well-defined transformations of system specifications (morphisms) that preserve the intended semantics and stated properties of the architecture under design. The aim of the present article is to review and summarize these formal, correct-by-construction, design transformations. Most of them are implemented in the POLYCHRONY tool-set, allowing for a mixed bottom–up and top–down design of an embedded hardware–software system using the SIGNAL design language.

    From the Greek "poly chronos" to mean multiple clocks.


    • A. Benveniste, P. Le Guernic and C. Jacquemot, Sci. Comput. Programming 16, (1991), DOI: 10.1016/0167-6423(91)90001-E. Google Scholar
    • G. Berry and G. Gonthier, Sci. Comput. Programming 19, (1992), DOI: 10.1016/0167-6423(92)90005-V. Google Scholar
    • N.   Halbwachs , Synchronous Programming of Reactive Systems ( Kluwer Academic Publishers , 1993 ) . CrossrefGoogle Scholar
    • N. Halbwachset al., Proc. IEEE 79, 9 (1991), DOI: 10.1109/5.97300. Google Scholar
    • E. A. Lee and A. Sangiovanni-Vincentelli, IEEE Trans. Computer-Aided Design 17, 12 (1998), DOI: 10.1109/43.736561. Google Scholar
    • D.   Nowak , J.-P.   Talpin and P.   Le Guernic , Synchronous structures , Int. Conf. Concurrency Theory . Google Scholar
    • A.   Benveniste et al. , A protocol for loosely time-triggered architectures , Embedded Software Conference ( Springer-Verlag , 2002 ) . Google Scholar
    • P. Caspi, Theoret. Comput. Sci. 94, (1992), DOI: 10.1016/0304-3975(92)90326-B. Google Scholar
    • P.   Caspi , A.   Girault and C.   Jard , Distributed reactive systems , Int. Conf. Parallel and Distributed Computing Systems ( ISCA , 1994 ) . Google Scholar
    • G. Berry and E. Sentovich, Formal Methods in Systems Design 17, 2 (2000). Google Scholar
    • P.   Aubry , Thèse de l'Université de Rennes 1 ( IFSIC , 1997 ) . Google Scholar
    • A. Benveniste, B. Caillaud and P. Le Guernic, Inform. Comput. 163, 125 (2000), DOI: 10.1006/inco.2000.9999. Crossref, ISIGoogle Scholar
    • L. P.   Carloni , K. L.   McMillan and A. L.   Sangiovanni-Vincentelli , Latency-insensitive protocols , Int. Conf. Computer-Aided Verification 1633 , Lecture Notes in Computer Science ( Springer-Verlag , 1999 ) . Google Scholar
    • T. P.   Amagbegnon , L.   Besnard and P.   Le Guernic , Implementation of the data-flow synchronous language SIGNAL , Conf. Programming Language Design and Implementation ( ACM Press , 1995 ) . Google Scholar
    • H. Marchandet al., Sci. Comput. Programming 41(1), 85 (2001), DOI: 10.1016/S0167-6423(00)00020-4. Crossref, ISIGoogle Scholar
    • H.-P.   Juan , V.   Chaiyakul and D.   Gajski , Condition graphs for high-quality behavioral synthesis , Int. Conf. Computer-Aided Design . Google Scholar
    • A.   Kountouris and C.   Wolinski , Hierarchical conditional dependency graphs as a unifying design representation in the CODESIS high-level synthesis system , Int. Symp. Syst. Synthesis . Google Scholar
    • G.   Lakshminarayana et al. , Transforming control-flow intensive designs to facilitate power management , Int. Conf. Computer-Aided Design . Google Scholar
    • S.   Gupta et al. , Speculation techniques for high-level synthesis of control-intensive designs , Design Automation Conference ( ACM Press , 2001 ) . Google Scholar