Behavioral Type Inference

Part II — Behavioral type inference for system design
  • Jean-Pierre Talpin
  • David Berner
  • Sandeep Kumar Shukla
  • Paul Le Guernic
  • Abdoulaye Gamatié
  • Rajesh Gupta


The design productivity gap has been recognized by the semiconductor industry as one of the major threats to the continued growth of system-on-chips and embedded systems. Ad-hoc system-level design methodologies, that lifts modeling to higher levels of abstraction, and the concept of intellectual property (IP), that promotes reuse of existing components, are essential steps to manage design complexity. However, the issue of compositional correctness arises with these steps. Given components from different manufacturers, designed with heterogeneous models, at different levels of abstraction, assembling them in a correct-by-construction manner is a difficult challenge. We address this challenge by proposing a process algebraic model to support system design with a formal model of computation and serve as a behavioral type system to capture the behavior of system components at the interface level. The proposed algebra is conceptually minimal, equipped with a formal semantics defined in a synchronous model of computation, and supports a scalable notion and a flexible degree of abstraction.

We demonstrate its benefits by considering the type-based synthesis of latency-insensitive protocols. We show that the synthesis of component wrappers can be optimized by the behavioral information carried by interface type descriptions and yields minimized stalls and maximized throughput.


Formal Method Finite Impulse Response Finite Impulse Response Filter Proof Obligation Type Inference 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Amagbegnon, T. P., Besnard, L., le Guernic, P. “Implementation of the data-flow synchronous language SIGNAL”. In Conference on Programming Language Design and Implementation. ACM Press, 1995.Google Scholar
  2. [2]
    J.T. Buck, S. Ha, E.A. Lee and D.G. Messerschmitt. Ptolemy: A Framework for Simulating and Prototyping Heterogeneous Systems. International Journal of Computer Simulation, special issue on “Simulation Software Development”v. 4, pp. 155–182. Ablex, April 1994.Google Scholar
  3. [3]
    E. Dijkstra “A Discipline of Programming”. Prentice Hall, 1976.Google Scholar
  4. [4]
    de Alfaro, L., Henzinger, T. A. “Interface theories for component-based design”. International Workshop on Embedded Software. Lecture Notes in Computer Science v. 2211. Springer-Verlag, 2001.Google Scholar
  5. [5]
    F. Doucet, S. Shukla, and R. Gupta. “Typing abstractions and management in a component framework”. Asia and South Pacific Design Automation Conference, January 2003.Google Scholar
  6. [6]
    Lee, E. A., Sangiovanni-Vincentelli, A. “A framework for comparing models of computation”. In IEEE transactions on computer-aided design, v. 17, n. 12. IEEE Press, December 1998.Google Scholar
  7. [7]
    le Guernic, P., Talpin, J.-P., le Lann, J.-L. Polychrony for system design. In Journal of Circuits, Systems and Computers. Special Issue on Application-Specific Hardware Design. World Scientific, 2002.Google Scholar
  8. [8]
    Mousavi, M., R., le Guernic, P., Talpin, J.-P., Shukla, S., Basten, T. Modeling and validation of asynchronous systems in synchronous frameworks. In Digital Automation and Test Europe. IEEE Press, February 2004.Google Scholar
  9. [9]
    Novillo, D. “Tree SSA, a new optimization infrastructure for GCC”. GCC developers summit, 2003.Google Scholar
  10. [10]
    Nowak, D., Beauvais, J.-R., Talpin, J.-P. “Co-inductive axiomatization of a synchronous language”. In International Conference on Theorem Proving in Higher-Order Logics. Lecture Notes in Computer Science, Springer Verlag, October 1998.Google Scholar
  11. [11]
    Nowak, D., Talpin, J.-P., le Guernic, P. “Synchronous structures”. In International Conference on Concurrency Theory. Lecture Notes in Computer Science, Springer Verlag, August 1999.Google Scholar
  12. [12]
    Pnueli, A., Shankar, N., Singerman, E. Fair synchronous transition systems and their liveness proofs. International School and Symposium on Formal Techniques in Real-time and Fault-tolerant Systems. Lecture Notes in Computer Science v. 1468. Springer Verlag, 1998.Google Scholar
  13. [13]
    S. K. Rajamani and J. Rehof, “A BEHAVIORAL MODULE SYSTEM FOR THE 7-CALCULUS”. Static Analysis Symposium. Lecture Notes in Computer Science. Springer Verlag, July 2001.Google Scholar
  14. [14]
    Talpin, J.-P., Gamatié, A., le Dez, B., Berner, D., le Guernic, P. “Hard real-time implementation of embedded systems in JAVA”. International Workshop on Scientific Engineering of Distributed JAVA Applications. Lecture Notes in Computer Science. Springer Verlag, November 2003.Google Scholar
  15. [15]
    J.-P. talpin, P. le guernic, S. K. shukla, R. gupta, and F. Doucet. “Polychrony for formal refinement-checking in a system-level design methodology”. Application of Concurrency to System Design. IEEE Press, June 2003.Google Scholar
  16. [16]
    J.-P. Talpin, P. le Guernic “Algebraic theory for behavioral type inference”. In Formal Methods and Models for System Design (this volume). Kluwer Academic Publishers, June 2004.Google Scholar
  17. [17]
    The Polychrony website., 2004.
  18. [18]
    The OSCI SystemC website., 2004.
  19. [19]
    The Gnu Compiler Collection (GCC)., 2004.
  20. [20]
    The GCC Tree-SSA Branch., 2004.

Copyright information

© Springer Science+Business Media Dordrecht 2004

Authors and Affiliations

  • Jean-Pierre Talpin
    • 1
  • David Berner
    • 1
  • Sandeep Kumar Shukla
    • 2
  • Paul Le Guernic
    • 1
  • Abdoulaye Gamatié
    • 1
  • Rajesh Gupta
    • 3
  1. 1.INRIA, project EspressoIRISA, Campus de BeaulieuRennes CedexFrance
  2. 2.Department of Electrical and Computer EngineeringVirginia TechBlacksburgUSA
  3. 3.Department of Computer Science and EngineeringUniversity of California et San DiegoLa JollaUSA

Personalised recommendations