Behavioral Type Inference
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.
KeywordsFormal Method Finite Impulse Response Finite Impulse Response Filter Proof Obligation Type Inference
Unable to display preview. Download preview PDF.
- 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
- 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
- E. Dijkstra “A Discipline of Programming”. Prentice Hall, 1976.Google Scholar
- 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
- 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
- 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
- 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
- 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
- Novillo, D. “Tree SSA, a new optimization infrastructure for GCC”. GCC developers summit, 2003.Google Scholar
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- The Polychrony website. http://www.irisa.fr/espresso/Polychrony, 2004.
- The OSCI SystemC website. http://www.SystemC.org, 2004.
- The Gnu Compiler Collection (GCC). http://www.gcc.gnu.org, 2004.
- The GCC Tree-SSA Branch. http://www.gcc.gnu.org/projects/tree-ssa, 2004.