Formal Modeling of Embedded Systems with Explicit Schedules and Routes



A main goal of compilation is to efficiently map application programs onto execution platforms, while hiding the details of the latter to the programmer through high-level programming languages. Of course this is only feasible inside a certain range of constructs, and the judicious design of sequential programming languages and computer architectures that match one another has been a decades-long process. Now the advent of multicore processors brings radical changes to this topic, bringing forth concurrency as a key element in efficiency, both for application design and architecture computing power. The shift is mostly prompted by technological factors, namely the ability to cram several processors on a single chip, and the diminishing gains of Instruction Level Parallelism techniques used in former architectures. Still, the definition of high-level programming (and more generally, application design) formalisms matching the new era is a largely unsolved issue.


Dependency Graph Relay Station Compilation Time Computation Node Input Place 
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.


  1. 1.
    S. Amarasinghe. A stream compiler for communication-exposed architectures. In Proceedings of ASPLOS, 2002.Google Scholar
  2. 2.
    F. Anceau. A synchronous approach for clocking VLSI systems. IEEE Journal of Solid-State Circuits, 17:51–56, 1982.CrossRefGoogle Scholar
  3. 3.
    C. André. Representation and analysis of reactive behaviors: A synchronous approach. In CESA, 1996.Google Scholar
  4. 4.
    F. Baccelli, G. Cohen, G. J. Olsder, and J.-P. Quadrat. Synchronization and Linearity. Wiley, Chichester, West Sussex, UK, 1992.zbMATHGoogle Scholar
  5. 5.
    D. Baneres, J. Cortadella, and M. Kishinevsky. Variable-latency design using function speculation. In Proc. Design, Automation and Test in Europe, April 2009.Google Scholar
  6. 6.
    L. Benini, E. Macii, and M. Poncino. Telescopic units: Increasing the average throughput of pipelined designs by adaptive latency control. In DAC, pages 22–27, 1997.Google Scholar
  7. 7.
    A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 91(1):64–83, 2003.CrossRefGoogle Scholar
  8. 8.
    S. S. Bhattacharyya, P. K. Murthy, and E. A. Lee. Software Synthesis from Dataflow Graphs. Kluwer, Dordrecht, 1996.zbMATHCrossRefGoogle Scholar
  9. 9.
    G. Bilsen, M. Engels, R. Lauwereins, and J. Peperstraete. Cyclo-static dataflow. IEEE Transactions on Signal Processing, 44:397–408, February 1996.CrossRefGoogle Scholar
  10. 10.
    A. Bouali. XEVE, an esterel verification environment. In CAV ’98: Proceedings of the 10th International Conference on Computer Aided Verification, pages 500–504, London, UK, 1998. Springer.Google Scholar
  11. 11.
    J. Boucaron, A. Coadou, and R. de Simone. Latency-insensitive design: retry relay-station and fusion shell. In Formal Methods for Globally Asynchronous Locally Synchronous Design 2009 Proceedings, 2009.Google Scholar
  12. 12.
    J. Boucaron, A. Coadou, B. Ferrero, J.-V. Millo, and R. de Simone. Kahn-extended event graphs. Research Report RR-6541, INRIA, 2008.Google Scholar
  13. 13.
    J. Boucaron, J.-V. Millo, and R. de Simone. Another glance at relay-stations in latency-insensitive design. In Formal Methods for Globally Asynchronous Locally Synchronous Design 2005 Proceedings, 2005.Google Scholar
  14. 14.
    J. Boucaron, J.-V. Millo, and R. de Simone. Latency-insensitive design and central repetitive scheduling. In Proceedings of the 4th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE’06), pages 175–183, Napa Valley, CA, USA, July 2006. IEEE Press.Google Scholar
  15. 15.
    J. Boucaron, J.-V. Millo, and R. de Simone. Formal methods for scheduling of latency-insensitive designs. EURASIP Journal on Embedded Systems, 2007(1), 8–8, 2007.CrossRefGoogle Scholar
  16. 16.
    R. G. Brown and P. Y. C. Hwang. Introduction to Random Signals and Applied Kalman Filtering, 3rd edition. Wiley, New York, 1996.Google Scholar
  17. 17.
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986.Google Scholar
  18. 18.
    J. T. Buck. Scheduling Dynamic Dataflow Graphs with Bounded Memory Using the Token Flow Model. PhD thesis, University of California, Berkeley, CA, USA, 1993.Google Scholar
  19. 19.
    D. Bufistov, J. Júlvez, and J. Cortadella. Performance optimization of elastic systems using buffer resizing and buffer insertion. In ICCAD ’08: Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, pages 442–448, Piscataway, NJ, USA, 2008. IEEE Press.Google Scholar
  20. 20.
    J. L. Campbell. Application of Airborne Laser Scanner – Aerial Navigation. PhD thesis, Russ College of Engineering and Technology, Athens, OH, USA, February 2006.Google Scholar
  21. 21.
    L. P. Carloni, K. L. McMillan, A. Saldanha, and A. L. Sangiovanni-Vincentelli. A methodology for correct-by-construction latency-insensitive design. In Proceedings of the International Conference on Computer-Aided Design (ICCAD’99), pages 309–315, Piscataway, NJ, USA, November 1999. IEEE.Google Scholar
  22. 22.
    L. P. Carloni, K. L. McMillan, and A. L. Sangiovanni-Vincentelli. Theory of latency-insensitive design. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 20(9):1059–1076, 2001.CrossRefGoogle Scholar
  23. 23.
    L. P. Carloni and A. L. Sangiovanni-Vincentelli. Performance analysis and optimization of latency insensitive systems. In DAC ’00: Proceedings of the 37th Annual Design Automation Conference, pages 361–367, New York, NY, USA, 2000. ACM.Google Scholar
  24. 24.
    L. P. Carloni and A. L. Sangiovanni-Vincentelli. Combining retiming and recycling to optimize the performance of synchronous circuits. In SBCCI ’03: Proceedings of the 16th symposium on Integrated circuits and systems design, page 47, Washington, DC, USA, 2003. IEEE Computer Society.Google Scholar
  25. 25.
    P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre: a declarative language for programming synchronous systems. In POPL, pages 178–188, 1987.Google Scholar
  26. 26.
    P. Caspi and M. Pouzet. A functional extension to Lustre. In M. A. Orgun and E. A. Ashcroft, editors, International Symposium on Languages for Intentional Programming, Sydney, Australia, May 1995. World Scientific.Google Scholar
  27. 27.
    P. Caspi and M. Pouzet. Lucid Synchrone, version 1.01. Tutorial and reference manual. Laboratoire d’Informatique de Paris 6, January 1999.Google Scholar
  28. 28.
    M. R. Casu and L. Macchiarulo. A detailed implementation of latency insensitive protocols. In Proceedings of the 1st Workshop on Globally Asynchronous, Locally Synchronous Design (FMGALS’03), pages 94–103, September 2003.Google Scholar
  29. 29.
    M. R. Casu and L. Macchiarulo. A new approach to latency insensitive design. In Proceedings of the 41st Annual Conference on Design Automation (DAC’04), pages 576–581, 2004.Google Scholar
  30. 30.
    M. R. Casu and L. Macchiarulo. Adaptive latency-insensitive protocols. IEEE Design and Test of Computers, 24(5):442–452, 2007.CrossRefGoogle Scholar
  31. 31.
    A. Cohen, M. Duranton, C. Eisenbeis, C. Pagetti, F. Plateau, and M. Pouzet. N-synchronous kahn networks: a relaxed model of synchrony for real-time systems. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06), pages 180–193, New York, NY, USA, January 2006. ACM.Google Scholar
  32. 32.
    F. Commoner, A. W. Holt, S. Even, and A. Pnueli. Marked directed graph. Journal of Computer and System Sciences, 5:511–523, October 1971.MathSciNetzbMATHCrossRefGoogle Scholar
  33. 33.
    J. Cortadella, M. Kishinevsky, and B. Grundmann. Synthesis of synchronous elastic architectures. In Proceedings of the 43rd Annual Conference on Design Automation (DAC’06), pages 657–662, New York, NY, USA, 2006. ACM.Google Scholar
  34. 34.
    M. Dall’Osso, G. Biccari, L. Giovannini, D. Bertozzi, and L. Benini. Xpipes: a latency insensitive parameterized network-on-chip architecture for multi-processor SOCS. In ICCD, pages 536–, 2003.Google Scholar
  35. 35.
    A. Darte, Y. Robert, and F. Vivien. Scheduling and Automatic Parallelization. Birkhaüser, Boston, 2000.zbMATHCrossRefGoogle Scholar
  36. 36.
    A. Dasdan and R. Gupta. Faster maximum and minimum mean cycle algorithms for system-performance analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(10):889–899, 1998.CrossRefGoogle Scholar
  37. 37.
    G. de Micheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill, New York, 1994.Google Scholar
  38. 38.
    N. Eén and N. Sörensson. An extensible SAT solver. In SAT Proceedings, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer, Berlin, 2003.Google Scholar
  39. 39.
    J. Eker, J. Janneck, E. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Y. Xiong. Taming heterogeneity – the Ptolemy approach. Proceedings of the IEEE, 91(1):127–144, 2003.CrossRefGoogle Scholar
  40. 40.
    M. Engels, G. Bilsen, R. Lauwereins, and J. A. Peperstraete. Cyclo-static dataflow: model and implementation. In Conference Record of the Twenty-Eighth Asilomar Conference on Signals, Systems and Computers, volume 1, pages 503–507, Pacific Grove, CA, USA, 1994.Google Scholar
  41. 41.
    D. Gebhardt and K. Stevens. Elastic flow in an application specific network-on-chip. In Formal Methods for Globally Asynchronous Locally Synchronous Design Proceedings, 2007.Google Scholar
  42. 42.
    R. Govindarajan and G. R. Gao. Rate-optimal schedule for multi-rate DSP computations. Journal of VLSI Signal Processing, 9(3):211–232, 1995.CrossRefGoogle Scholar
  43. 43.
    T. Grandpierre and Y. Sorel. From algorithm and architecture specification to automatic generation of distributed real-time executives: a seamless flow of graphs transformations. In Proceedings of First ACM and IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE’03, Mont Saint-Michel, France, June 2003.Google Scholar
  44. 44.
    C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666–677, 1978.MathSciNetzbMATHCrossRefGoogle Scholar
  45. 45.
    G. Hoover and F. Brewer. Synthesizing synchronous elastic flow networks. In DATE, pages 306–311, 2008.Google Scholar
  46. 46.
    D. B. Johnson. Finding all the elementary circuits of a directed graph. SIAM Journal on Computing, 4(1):77–84, 1975.MathSciNetzbMATHCrossRefGoogle Scholar
  47. 47.
    G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information Processing ’74: Proceedings of the IFIP Congress, pages 471–475, New York, NY, USA, 1974. North-Holland.Google Scholar
  48. 48.
    M. Karczmarek. Phased scheduling of stream programs. In Proceedings of LCTES, 2003.Google Scholar
  49. 49.
    R. Karp. A characterization of the minimum cycle mean in a digraph. Discrete Mathematics, 23(3):309–311, 1978.MathSciNetzbMATHCrossRefGoogle Scholar
  50. 50.
    R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147–195, May, 1969.MathSciNetzbMATHCrossRefGoogle Scholar
  51. 51.
    K. Kennedy and J. R. Allen. Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann, San Francisco, CA, USA, 2002.Google Scholar
  52. 52.
    M. Kudlur and S. A. Mahlke. Orchestrating the execution of stream programs on multicore platforms. In PLDI, pages 114–124, 2008.Google Scholar
  53. 53.
    P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann. Polychrony for system design. Journal for Circuits, Systems and Computers, 12:261–304, 2002.Google Scholar
  54. 54.
    C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell Systems Technical Journal, 38:985–999, 1959.Google Scholar
  55. 55.
    E. A. Lee and D. G. Messerschmitt. Static scheduling of synchronous data flow programs for digital signal processing. IEEE Transactions on Computers, C-36(1):24–35, 1987.Google Scholar
  56. 56.
    E. A. Lee and D. G. Messerschmitt. Synchronous data flow. Proceeding of the IEEE, 75(9):1235–1245, 1987.CrossRefGoogle Scholar
  57. 57.
    C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1):5–35, 1991.MathSciNetzbMATHCrossRefGoogle Scholar
  58. 58.
    B. Lickly, I. Liu, S. Kim, H. D. Patel, S. A. Edwards, and E. A. Lee. Predictable programming on a precision timed architecture. In Proceedings of Compilers, Architectures, and Synthesis of Embedded Systems (CASES), Atlanta, Georgia, USA, October 19–24, 2008.Google Scholar
  59. 59.
    N. Liveris, C. Lin, J. Wang, H. Zhou, and P. Banerjee. Retiming for synchronous data flow graphs. In ASP-DAC ’07: Proceedings of the 2007 Asia and South Pacific Design Automation Conference, pages 480–485, Washington, DC, USA, 2007. IEEE Computer Society.Google Scholar
  60. 60.
    O. Marchetti and A. Munier-Kordon. Minimizing place capacities of weighted event graphs for enforcing liveness. Discrete Event Dynamic Systems, 18(1):91–109, 2008.MathSciNetzbMATHCrossRefGoogle Scholar
  61. 61.
    O. Marchetti and A. Munier-Kordon. A sufficient condition for the liveness of weighted event graphs. European Journal of Operational Research, 197(2):532–540, 2009.MathSciNetzbMATHCrossRefGoogle Scholar
  62. 62.
    K. L. McMillan. Symbolic Model Checking. Kluwer, Dordrecht, 1993.zbMATHCrossRefGoogle Scholar
  63. 63.
    T. O’Neil and E.-M. Sha. Retiming synchronous data-flow graphs to reduce execution time. IEEE Transactions on Signal Processing, 49(10):2397–2407, 2001.MathSciNetCrossRefGoogle Scholar
  64. 64.
    H. D. Patel and S. K. Shukla. SystemC Kernel Extensions For Heterogenous System Modeling: A Framework for Multi-MoC Modeling and Simulation. Kluwer, Norwell, MA, USA, 2004.Google Scholar
  65. 65.
    C. A. Petri. Kommunikation mit Automaten. PhD thesis, Institut für instrumentelle Mathematik, Bonn, Germany, 1962.Google Scholar
  66. 66.
    D. Potop-Butucaru, S. A. Edwards, and G. Berry. Compiling Esterel. Springer, Berlin, 2007.Google Scholar
  67. 67.
    J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming, 1982.Google Scholar
  68. 68.
    C. Ramchandani. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets. PhD thesis, Dept. of Electrical Engineering, Massachusetts Institute of Technology, Cambridge, MA, USA, 1973.Google Scholar
  69. 69.
    M. D. Riedel. Cyclic Combinational Circuits. PhD thesis, Dept. of Electrical Engineering, California Institute of Technology, Pasadena, CA, USA, November 2003.Google Scholar
  70. 70.
    K. Schneider. The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, 2009.Google Scholar
  71. 71.
    J. Sermulins. Cache aware optimization of stream programs. In Proceedings of LCTES, 2005.Google Scholar
  72. 72.
    C. Soviani, O. Tardieu, and S. A. Edwards. High-level optimization by combining retiming and shannon decomposition. In In Proceedings of the International Workshop on Logic and Synthesis (IWLS), Lake Arrowhead, CA, June, 2005.Google Scholar
  73. 73.
    S. Suhaib, D. Mathaikutty, D. Berner, and S. K. Shukla. Validating families of latency insensitive protocols. IEEE Transactions on Computers, 55(11):1391–1401, 2006.CrossRefGoogle Scholar
  74. 74.
    S. Suhaib, D. Mathaikutty, S. K. Shukla, D. Berner, and J.-P. Talpin. A functional programming framework for latency insensitive protocol validation. Electronic Notes in Theoretical Computer Science, 146(2):169–188, 2006.CrossRefGoogle Scholar
  75. 75.
    C. Svensson. Synchronous latency insensitive design. In Proc. of 10th IEEE International Symposium on Asynchronous Circuits and Systems, 2004.Google Scholar
  76. 76.
    W. Thies, M. Karczmarek, M. Gordon, D. Maze, J. Lin, A. Meli, A. Lamb, C. Leger, and S. Amarasinghe. Streamit: a language for streaming applications. In Proceedings of New England Programming Languages and Systems Symposium (NEPLS), 2002.Google Scholar

Copyright information

© Springer US 2010

Authors and Affiliations

  1. 1.INRIA Sophia Antipolis MéditerranéeSophia AntipolisFrance

Personalised recommendations