System Level Design and Verification Using a Synchronous Language

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

System Level Design and Verification Using a Synchronous Language

Full text

Pdf (434 KB)

Source

International Conference on Computer Aided Design archive
Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design table of contents

Page: 433

Year of Publication: 2003

ISBN ~ ISSN:1092-3152 , 1-58113-762-1

Authors

Gérard Berry	Esterel Technologies, France
Michael Kishinevsky	Intel Corp., Hillsboro, OR
Satnam Singh	Xilinx, San Jose, CA

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

IEEE Computer Society Washington, DC, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 42, Citation Count: 3

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	10.1109/ICCAD.2003.135

ABSTRACT

Synchronous languages such as Esterel, Lustre, Signal, andothers were originally developed for safety-critical embedded software and compiled into C. They have recently been extended to hardware with new language features and compilers to RTL. Contrary to traditional HDL languages (Verilog, VHDL) and recent system-level languages (SystemC, System Verilog), they have well defined formal semantics,which facilitate bug avoidance using correct-by-constructioncompilation and verification techniques.The tutorial will demonstrate what the synchronous language offers for the modeling, design, analysis and implementation of systems that comprise hardware and software.It will be based on Esterel. Esterel models have proved tobe useful for rapid design space exploration and verificationat system level, without resorting to detailed implementation and slow bit-level event-based simulation. We show how to model control-dominated IP blocks at a higher levelof abstraction and how to use the target C code or RTL inconjunction with other system-level tools. Case studies include examples of design space exploration by synthesizing equivalent hardware or software from the same Esterel description, with formal verification of safety properties such as bus protocol conformance. We conclude with a review of future research directions.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	[1] SystemC, 2002, website at http://www.systemc.org.
	2	[2] UCI, SpecC, 2002, website at http://ics.uci.edu/ specc.
	3	Gérard Berry, The foundations of Esterel, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
	4	[4] C. André, "Representation and analysis of reactive behaviors: A synchronous approach," in Proc. CESA'96, Lille, France, July 1996.
	5	[5] G. Berry, The Esterel v5_91 Primer. Draft book, available at http://www.esterel-technologies.com, version 3, August 2000.
	6	[6] Esterel Studio 5.0 reference manual, Esterel Technologies, 2003.
	7	[7] G. Berry and M. Kishinevsky, "Hardware Esterel language extension proposal," Tech. Rep., August 2000, available at http://www.esterel-technologies.com.
	8	K. Schneider, Embedding Imperative Synchronous Languages in Interactive Theorem Provers, Proceedings of the Second International Conference on Application of Concurrency to System Design, p.143, June 25-29, 2001
	9	[9] Virtex^TM-II Platform FPGA Handbook, Xilinx Inc., December 2000.
	10	[10] Xilinx, Aurora Technology Overview, 2003.
	11	[11] CoWare, 2003, website at http://www.coware.com.
	12	[12] S. Singh, "Design and verification of CoreConnect^TM IP using Esterel," the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, L'Aquila, Italy, 2003.
	13	[13] IBM, The CoreConnect^TM Bus Architecture, 1999.

CITED BY 3

	Tero Kangas , Petri Kukkala , Heikki Orsila , Erno Salminen , Marko Hännikäinen , Timo D. Hämäläinen , Jouni Riihimäki , Kimmo Kuusilinna, UML-based multiprocessor SoC design framework, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.2, p.281-320, May 2006
	Tarvo Raudvere , Ingo Sander , Axel Jantsch, A synchronization algorithm for local temporal refinements in perfectly synchronous models with nested feedback loops, Proceedings of the 17th great lakes symposium on Great lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy
	Tarvo Raudvere , Ingo Sander , Axel Jantsch, Synchronization after design refinements with sensitive delay elements, Proceedings of the 5th IEEE/ACM international conference on Hardware/software codesign and system synthesis, September 30-October 03, 2007, Salzburg, Austria