Hardware/software synthesis of formal specifications in codesign of embedded systems

ABSTRACT

CoDesign aims to integrate the design techniques of hardware and software. In this work, we present a CoDesign methodology based on a formal approach to embedded system specification. This methodology uses the Templated T-LOTOS language to specify the system during all design phases. Templated T-LOTOS is a formal language based on CCS and CSP models. Using Templated T-LOTOS, a system can be specified by observing the temporal ordering in which the events occur from the outside. In this paper we focus on the synthesis of system specified by Templated T-LOTOS. The proposed synthesis algorithm takes advantage of peculiarities of Templates T-LOTOS. Hardware modules are translated into a register transfer-level language that manages some signals in order to drive synchronization, while the software models are translated into C according to a finite state model whose operations are controlled by a scheduler. The synthesis of the Templated T-LOTOS specification is based on the direct translation of the language operators to ensure that the implemented system is the same as the specified one.

REFERENCES

• 1: Jay K. Adams , Donald E. Thomas, Multiple-process behavioral synthesis for mixed hardware-software systems, Proceedings of the 8th international symposium on System synthesis, p.10-15, September 13-15, 1995, Cannes, France [doi>10.1145/224486.224489]
• 2: Jakob Axelsson, Hardware/software partitioning aiming at fulfillment of real-time constraints, Journal of Systems Architecture: the EUROMICRO Journal, v.42 n.6-7, p.449-464, Dec. 1, 1996 [doi>10.1016/S1383-7621(96)00033-1]
• 3: BERRY, a., COURONNE, P., AND GONTHIER, a. 1991. The synchronous approach to reactive and real-time systems. Proc. IEEE 79.
• 4: BERRY, G. AND TOUATI, H. 1993. Optimized controller synthesis using Esterelle. In Proceedings of the International Workshop on Logic Synthesis (May),
• 5: Tommaso Bolognesi , Ed Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, v.14 n.1, p.25-59, March, 1987 [doi>10.1016/0169-7552(87)90085-7]
• 6: BOYER, R. S., KAUFMANN, M., AND MOORE, J. S. 1995. The Boyer-Moore theorem prover and its interactive enhancements. In Computers & Mathematics with Applications Pergamon Press, Inc., London, UK, 27-62.
• 7: BRINKSMA, E., SCOLLO, G., AND VISSERS, C. 1987. Experience with and future of LOTOS as a specification language. Tech. Rep. INF-87-17. Twente University.
• 8: CARCHIOLO, V., MALGERI, M., AND MANGIONI, G. 1996. TTL: A LOTOS extension for system description. In Proceedings of the Conference on Basys (Basys '96, Lisbon, Portugal),
• 9: CARCHIOLO, V., MALGERI, M., AND MANGIONI, G. 1998. Formal codesign methodology with multistep partitioning. J. Comput. Aided VLSI Des. 7, 4.
• 10: CARCHIOLO, V., MALGERI, M., AND MANGIONI, G. 1998. Synthesis of TTL specification: A case study. In Proceedings of the MultiConference on CESA98-IMACS,
• 11: 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]
• 12: V. Catania , N. Fiorito , M. Malgeri , M. Russo, A framework for codesign based on fuzzy logic and genetic algorithms, Proceedings of the 8th international conference on Industrial and engineering applications of artificial intelligence and expert systems, p.797-804, June 05-09, 1995, Melbourne, Australia
• 13: Vincenzo Catania , Michele Malgeri , Marco Russo, Applying Fuzzy Logic to Codesign Partitioning, IEEE Micro, v.17 n.3, p.62-70, May 1997 [doi>10.1109/40.591657]
• 14: Massimiliano Chiodo , Paolo Guisto , Attila Jurecska , Luciano Lavagno , Ellen Sentovich , Harry Hsieh , Kei Suzuki , Alberto Sangiovanni-Vincentelli, Synthesis of software programs for embedded control application, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.587-592, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217594]
• 15: CHIODO, M., GIUSTO, P., JURESKA, A., HSIEH, H. C., SANGIOVANNI-VINCENTELLI, A., AND LAVAGNO, L. 1993. A formal specification model for hardware/software codesign. In Proceedings of the International Workshop on Hardware-Software Codesign (Boston, MA, Sept.),
• 16: Pai H. Chou , Ross B. Ortega , Gaetano Borriello, The Chinook hardware/software co-synthesis system, Proceedings of the 8th international symposium on System synthesis, p.22-27, September 13-15, 1995, Cannes, France [doi>10.1145/224486.224491]
• 17: Pai Chou , Elizabeth A. Walkup , Gaetano Borriello, Scheduling for Reactive Real-Time Systems, IEEE Micro, v.14 n.4, p.37-47, August 1994 [doi>10.1109/40.296156]
• 18: Giovanni De Micheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill Higher Education, 1994
• 19: DRUSINSKI, D. AND HAR'EL, D. 1989. Using statecharts for hardware description and synthesis. IEEE Trans. Comput.-Aided Des. 8.
• 20: H. Ehrig , Bernd Mahr, Fundamentals of algebraic specification 2: module specifications and constraints, Springer-Verlag New York, Inc., New York, NY, 1990
• 21: ERNST, R. 1993. Hardware-software codesign of embedded controllers based on hardware extraction. In Proceedings of the International Workshop on Hardware-Software Codesign (Boston, MA, Sept.),
• 22: Rolf Ernst , Jorg Henkel , Thomas Benner, Hardware-Software Cosynthesis for Microcontrollers, IEEE Design & Test, v.10 n.4, p.64-75, October 1993 [doi>10.1109/54.245964]
• 23: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 24: GUERNIC, P. L., BENVENISTE, A., BOURNAT, P., AND GAUTHIER, T. 1985. A data flow oriented language for signal processing. IRISA Tech. Rep. 246. IRISA, Rennes, France.
• 25: R. K. Gupta , C. N. Coelho, Jr. , G. De Micheli, Synthesis and simulation of digital systems containing interacting hardware and software components, Proceedings of the 29th ACM/IEEE conference on Design automation, p.225-230, June 08-12, 1992, Anaheim, California, United States
• 26: Rajesh K. Gupta , Claudionor N. Coelho, Jr. , Giovanni De Micheli, Program Implementation Schemes for Hardware-Software Systems, Computer, v.27 n.1, p.48-55, January 1994 [doi>10.1109/2.248880]
• 27: Rajesh K. Gupta , Giovanni De Micheli, Hardware-Software Cosynthesis for Digital Systems, IEEE Design & Test, v.10 n.3, p.29-41, July 1993 [doi>10.1109/54.232470]
• 28: Rajesh K. Gupta , Giovanni De Micheli, Constrained software generation for hardware-software systems, Proceedings of the 3rd international workshop on Hardware/software co-design, September 22-24, 1994, Grenoble, France
• 29: Wolfgang A. Halang , Alexander D. Stoyenko, Constructing Predictable Real Time Systems, Kluwer Academic Publishers, Norwell, MA, 1991
• 30: Harry Hsieh , Alberto Sangiovanni-Vincentelli, Modeling micro-controller peripherals for high-level co-simulation and synthesis, Proceedings of the 5th International Workshop on Hardware/Software Co-Design, p.127, March 24-26, 1997
• 31: Jörg Henkel , Thomas Benner , Rolf Ernst , Wei Ye , Nikola Serafimov , Gernot Glawe, COSYMA: a software-oriented approach to hardware/software codesign, Journal of Computer and Software Engineering, v.2 n.3, p.293-314, 1994
• 32: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 33: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 34: ISO. 1988. Information processing systems, open system interconnection LOTOS, A formal description technique based on the temporal ordering of observational behaviour. ISO-IS-8807.
• 35: Kurt Keutzer, Hardware/software co-simulation, Proceedings of the 31st annual conference on Design automation, p.439-440, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196458]
• 36: Zvi Kohavi , Richard W. Hamming , Edward A. Feigenbaum, Switching and Finite Automata Theory: Computer Science Series, McGraw-Hill Higher Education, 1990
• 37: David Ku , Giovanni DeMicheli, HardwareC -- A Language for Hardware Design (Version 2.0), Stanford University, Stanford, CA, 1990
• 38: Sanjaya Kuman , James H. Aylor , Barry W. Johnson , Wm. A. Wulf, A Framework for Hardware/Software Codesign, Computer, v.26 n.12, p.39-45, December 1993 [doi>10.1109/2.247650]
• 39: KURSHAN, R. P. 1994. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton, NJ.
• 40: Luigi Logrippo , Tim Melanchuk , Robert J. Du Wors, The algebraic specification language LOTOS: an industrial experience, Conference proceedings on Formal methods in software development, p.59-66, May 09-11, 1990, Napa, California, United States
• 41: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 42: J. Quemada , S. Pavon , A. Fernandez, State exploration by transformation with LOLA, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.294-302, February 1990, Grenoble, France
• 43: Jared R. W. Smith , Rick Reed, Telecommunications Systems Engineering Using SDL, Elsevier Science Inc., New York, NY, 1989
• 44: Youngsoo Shin , Kiyoung Choi, Enforcing Schedulability of Multi-Task Systems by Hardware-Software Codesign, Proceedings of the 5th International Workshop on Hardware/Software Co-Design, p.3, March 24-26, 1997
• 45: Elizer Sternheim , Rajvir Singh , Yatin Trivedi, Digital Design with VERILOG HDL, Automata Publishing Company, 1991
• 46: Andrés Takach , Wayne Wolf , Miriam Leeser, An Automaton Model for Scheduling Constraints in Synchronous Machines, IEEE Transactions on Computers, v.44 n.1, p.1-12, January 1995 [doi>10.1109/12.368014]
• 47: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 48: Frank Vahid, Modifying Min-Cut for Hardware and Software Functional Partitioning, Proceedings of the 5th International Workshop on Hardware/Software Co-Design, p.43, March 24-26, 1997
• 49: VAN EIJK, P. 1989. Tools for LOTOS specification style transformation. Tech. Rep. Memo. 89-35.
• 50: VISSERS, C. A., SCOLLO, G., AND VAN SINDEREN, M. 1988. Architecture and specification style in formal description of distributed systems. In Proceedings of the Conference on Protocol Specification, Testing and Verification (Amsterdam), North-Holland Publishing Co., Amsterdam, The Netherlands, 189-204.
• 51: Alan S. Wenban , John W. O'Leary , Geoffrey M. Brown, Codesign of Communication Protocols, Computer, v.26 n.12, p.46-52, December 1993 [doi>10.1109/2.247651]
• 52: John Wilson, Hardware/software selected cycle solution, Proceedings of the 3rd international workshop on Hardware/software co-design, September 22-24, 1994, Grenoble, France

INDEX TERMS

Primary Classification:
  B. Hardware

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION

  C. Computer Systems Organization

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Design, Verification

Keywords:
codesign, embedded system, hardware and software synthesis