SHIM: a deterministic model for heterogeneous embedded systems

ABSTRACT

Typical embedded hardware/software systems are implemented using a combination of C and an hdl such as Verilog. While each is well-behaved in isolation, combining the two gives a nondeterministic model whose ultimate behavior must be validated through expensive (cycle-accurate) simulation.We propose an alternative for describing such systems. Our shim (software/hardware integration medium) model, effectively Kahn networks with rendezvous communication, provides deterministic concurrency. We present the Tiny-shim language for such systems and its semantics, demonstrate how to implement it in hardware and software, and discuss how it can be used to model a real-world system.By providing a powerful, deterministic formalism for expressing systems, designing systems and verifying their correctness will become easier.

REFERENCES

• 1: Felice Balarin , Massimiliano Chiodo , Paolo Giusto , Harry Hsieh , Attila Jurecska , Luciano Lavagno , Claudio Passerone , Alberto Sangiovanni-Vincentelli , Ellen Sentovich , Kei Suzuki , Bassam Tabbara, Hardware-software co-design of embedded systems: the POLIS approach, Kluwer Academic Publishers, Norwell, MA, 1997
• 2: Felice Balarin , Yosinori Watanabe , Harry Hsieh , Luciano Lavagno , Claudio Passerone , Alberto Sangiovanni-Vincentelli, Metropolis: An Integrated Electronic System Design Environment, Computer, v.36 n.4, p.45-52, April 2003 [doi>10.1109/MC.2003.1193228 ]
• 3: Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul~Le Guernic, and Robert de~Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 91(1):64--83, January 2003. Invited.
• 4: Gérard Berry, Esterel on hardware, Mechanized reasoning and hardware design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 5: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V ]
• 6: Gérard Berry , Ellen M. Sentovich, An Implementation of Constructive Synchronous Programs in POLIS, Formal Methods in System Design, v.17 n.2, p.135-161, Oct. 2000 [doi>10.1023/A:1008796718837 ]
• 7: Shuvra S. Bhattacharyya, Ranier Leupers, and Peter Marwedel. Software synthesis and code generation for signal processing systems. IEEE Transactions on Circuits and Systems---II: Analog and Digital Signal Processing, 47(9):849--875, September 2000.
• 8: Joseph T. Buck, Soonhoi Ha, Edward A. Lee, and David G. Messerschmitt. Ptolemy: A framework for simulating and prototyping heterogeneous systems. International Journal of Computer Simulation, 4:155--182, April 1994.
• 9: Joseph Tobin Buck , Edward A. Lee, Scheduling dynamic dataflow graphs with bounded memory using the token flow model, 1993
• 10: P. Caspi , D. Pilaud , N. Halbwachs , J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.178-188, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41641]
• 11: Massimiliano Chiodo, Paolo Giusto, Attila Jurecska, Luciano Lavagno, Harry Hsieh, and Alberto Sangiovanni-Vincentelli. A formal specification model for hardware/software codesign. In Proceeding of the International Workshop on Hardware-Software Codesign, Cambridge, Massachusetts, October 1993.
• 12: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 13: Stephen A. Edwards, Tony Ma, and Robert Damiano. Using a hardware model checker to verify software. In Proceedings of the 4th International Conference on ASIC (ASICON), Shanghai, China, October 2001.
• 14: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 15: Lilian Janin, Andrew Bardsley, and Doug~A. Edwards. Simulation and analysis of synthesised asynchronous circuits. International Journal of Simulation Systems, Science & Technology, 4(3--4):31--43, 2003.
• 16: Mark B. Josephs, Receptive process theory, Acta Informatica, v.29 n.1, p.17-31, Feb. 1992 [doi>10.1007/BF01178564]
• 17: Mark B. Josephs, An Analysis of Determinacy Using a Trace-Theoretic Model of Asynchronous Circuits, Proceedings of the 9th International Symposium on Asynchronous Circuits and Systems, p.121, May 12-15, 2003
• 18: Gilles Kahn. The semantics of a simple language for parallel programming. In Information Processing 74: Proceedings of IFIP Congress 74, pages 471--475, Stockholm, Sweden, August 1974. North-Holland.
• 19: Richard M. Karp and Raymond E. Miller. Properties of a model for parallel computations: Determinacy, termination, and queueing. SIAM Journal on Applied Mathematics, 14(6):1390--1411, November 1966.
• 20: Paul Le Guernic, Thierry Gautier, Michel Le Borgne, and Claude Le Maire. Programming real-time applications with SIGNAL. Proceedings of the IEEE, 79(9):1321--1336, September 1991.
• 21: Edward Ashford Lee , David G. Messerschmitt, Static scheduling of synchronous data flow programs for digital signal processing, IEEE Transactions on Computers, v.36 n.1, p.24-35, Jan. 1987
• 22: Edward A. Lee and David G. Messerschmitt. Synchronous data flow. Proceedings of the IEEE, 75(9):1235--1245, September 1987.
• 23: B. Lin, Efficient compilation of process-based concurrent programs without run-time scheduling, Proceedings of the conference on Design, automation and test in Europe, p.211-217, February 23-26, 1998, Le Palais des Congrés de Paris, France
• 24: Tadao Murata. Petri nets: Properties, analysis, and applications. Proceedings of the IEEE, 77(4):541--580, April 1989.
• 25: Thomas Martyn Parks, Bounded scheduling of process networks, University of California at Berkeley, Berkeley, CA, 1996
• 26: Kees van Berkel, Handshake circuits: an asynchronous architecture for VLSI programming, Cambridge University Press, New York, NY, 1993
• 27: Compositional Software Synthesis of Communicating Processes, Proceedings of the 1999 IEEE International Conference on Computer Design, p.646, October 10-13, 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

Keywords:
deterministic model of computation, hardware synthesis, hardware/software codesign, software synthesis