research-article

A Formal Approach to Incremental Converter Synthesis for System-on-Chip Design

Authors:

Gregor Goessler,

Partha S. RoopAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 20, Issue 1

Article No.: 13, Pages 1 - 30

https://doi.org/10.1145/2663344

Published: 18 November 2014 Publication History

Abstract

A system-on-chip (SoC) contains numerous intellectual property blocks, or IPs. Protocol mismatches between IPs may affect the system-level functionality of the SoC. Mismatches are addressed by introducing converters to control inter-IP interactions. Current approaches towards converter generation find limited practical application as they use restrictive models, lack formal rigour, handle a small subset of commonly encountered mismatches, and/or are not scalable. We propose a formal technique for SoC design using incremental converter synthesis. The proposed formulation provides precise models for protocols and requirements, and provides a scalable algorithm that allows adding multiple components and requirements to an SoC incrementally. We prove that the technique is sound and complete. Experimental results obtained using real-life AMBA benchmarks show the scalability and wide range of mismatches handled by our approach.

References

[1]

Janaki Akella and Kenneth McMillan. 1991. Synthesizing converters between finite state protocols. In Proceedings of the IEEE International Conference on Computer Design on VLSI in Computer and Processors (ICCD'91). 410--413.

Digital Library

[2]

Vassilis Androutsopoulos, D. M. Brookes, and Thomas J. W. Clarke. 2004. Protocol converter synthesis. IEE Proc. Comput. Digital Techn. 151, 6, 391--401.

[3]

ARM. 2011. AMBA 4 specifications. www.arm.com.

[4]

Karin Avnit, Vijay D'Silva, Arcot Sowmya, S. Ramesh, and Sri Parameswaran. 2009. Provably correct on-chip communication: A formal approach to automatic protocol converter synthesis. ACM Trans. Des. Autom. Electron. Syst. 14, 2.

Digital Library

[5]

Anupam Basu, Raj S. Mitra, and Peter Marwedel. 1998. Interface synthesis for embedded applications in a co-design environment. In Proceedings of the 11^th International Conference on VLSI Design: VLSI for Signal Processing (VLSID'98). 85--90.

Digital Library

[6]

Edith Beigne, Fabien Clermidy, Sylvain Miermont, and Pascal Vivet. 2008. Dynamic voltage and frequency scaling architecture for units integration within a gals noc. In Proceedings of the 2^nd ACM/IEEE International Symposium on Networks-on-Chip (NOCS'08). IEEE Computer Society, 129--138.

Digital Library

[7]

Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicholas Halbwachs, Paul Le Guernic, and Robert De Simone. 2003. The synchronous languages 12 years later. Proc. IEEE 91, 1, 64--83.

[8]

Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Richard Hull, and Massimo Mecella. 2005. Automatic composition of transition-based semantic web services with messaging. In Proceedings of the 31^st International Conference on Very Large Data Bases (VLDB'05). VLDB Endowment, 613--624.

Digital Library

[9]

Reinaldo A. Bergamashi, Subhrajit Bhattacharya, Jean-Marc R. Daveau, and William R. Lee. 2002. Methods and arrangements for automatic synthesis of systems-on-chip. US Patent 6,477,691. http://www.google.com/patents/US6477691.

[10]

Gaetano Borriello. 1988. A new interface specification methodology and its application to transducer synthesis. Ph.D. dissertation, University of California, Berkeley.

Digital Library

[11]

Gaetano Borriello and Randy H. Katz. 1987. Synthesis and optimization of interface transducer logic. In Proceedings of the International Conference on Computer Aided Design (ICCAD'87). 481--494.

[12]

Jing Cao and Albert Nymeyer. 2009. Formally synthesising a protocol converter: A case study. In Proceedings of the 14^th International Conference on Implementation and Application of Automata (CIAA'09). Springer, 249--252.

Digital Library

[13]

Krishnendu Chatterjee and Laurent Doyen. 2010. Energy parity games. In Proceedings of the 37^th International Colloquium on Automata, Languages and Programming (ICALP'10), Part 2. Springer, 599--610.

Digital Library

[14]

Krishnendu Chatterjee, Tom Henzinger, and Nir Piterman. 2006. Algorithms for buchi games. http://chess.eecs.berkeley.edu/pubs/238.html.

[15]

Jean-Marc Daveau, Gilberto Fernandes Marchioro, Tarek Ben-Ismail, and Ahmed Amine Jerraya. 1997. Protocol selection and interface generation for hw-sw codesign. IEEE Trans. Very Large Scale Integr. Syst. 5, 1, 136--144.

Digital Library

[16]

Luca de Alfaro and Thomas A. Henzinger. 2001. Interface automata. SIGSOFT Softw. Engin. Not. 26, 5, 109--120.

Digital Library

[17]

Rostislav Dobkin, Ran Ginosar, and Christos P. Sotiriou. 2004. Data synchronization issues in gals socs. In Proceedings of the 10^th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'04). 170--179.

[18]

Vijay D'Silva, S. Ramesh, and Arcot Sowmya. 2004a. Bridge over troubled wrappers: Automated interface synthesis. In Proceedings of the 17^th International Conference on VLSI Design (VLSID'04). 189--194.

Digital Library

[19]

Vijay D'Silva, S. Ramesh, and Arcot Sowmya. 2004b. Synchronous protocol automata: A framework for modelling and verification of soc communication architectures. In Proceedings of the Design, Automation, and Test in Europe Conference (DATE'04). 390--395.

Digital Library

[20]

Vijay D'Silva, S. Ramesh, and Arcot Sowmya. 2005. Synchronous protocol automata: A framework for modelling and verification of soc communication architectures. IEE Proc. Comput. Digital Techn. 152, 1, 20--27.

[21]

Emil Dumitrescu, Alain Girault, Herve Marchand, and Eric Rutten. 2007. Optimal discrete controller synthesis for the modeling of fault-tolerant distributed systems. In Proceedings of the IFAC Workshop on Dependable Control of Discrete Systems.

[22]

Masahiro Fujita, Hideo Tanida, Fei Gao, Tasuku Nishihara, and Takeshi Matsumoto. 2010. Synthesis and formal verification of on-chip protocol transducers through decomposed specification. In Proceedings of the 11^th International Symposium on Quality Electronic Design (ISQED'10). IEEE, 515--523.

[23]

Andreas Gerstlauer, Dongwan Shin, Junyu Peng, Rainer Domer, and Daniel D. Gajski. 2007. Automatic layer-based generation of system-on-chip bus communication models. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 26, 9, 1676--1687.

Digital Library

[24]

Christian Gierds, Arjan J. Mooij, and Karsten Wolf. 2012. Reducing adapter synthesis to controller synthesis. IEEE Trans. Serv. Comput. 5, 1, 72--85.

Digital Library

[25]

Paul Glover. 2005. Using and creating interrupt-based systems. http://www.xilinx.com/support/documentation/application_notes/xapp778.pdf.

[26]

Yashdeep Godhal, Krishnendu Chatterjee, and Thomas A. Henzinger. 2011. Synthesis of amba ahb from formal specification: A case study. Int. J. Softw. Tools Technol. Transfer 15, 5--6, 585--601.

[27]

Paul Green Jr. 1986. Protocol conversion. IEEE Trans. Comm. 34, 3, 257--268.

[28]

George T. Heineman and William T. Councill. 2001. Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley Longman.

Digital Library

[29]

Rick Hofmann and Ben Drerup. 2002. Next generation coreconnect processor local bus architecture. In Proceedings of the 15^th Annual IEEE International ASIC/SOC Conference. 221--225.

[30]

Michael Keating and Pierre Bricaud. 2002. Reuse Methodology Manual: For System-on-a-Chip Designs. Springer.

Digital Library

[31]

Ratnesh Kumar and Sudhir Nelvagal. 1996. Protocol conversion using supervisory control techniques. In Proceedings of the IEEE International Symposium on Computer-Aided Control System Design (CACSD'96). 32--37.

[32]

Ratnesh Kumar, Sudhir Nelvagal, and Steven I. Marcus. 1997. A discrete event systems approach for protocol conversion. Discr. Event Dynamic Syst. 7, 3, 295--315.

Digital Library

[33]

Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. 2001. Module checking. Inf. Comput. 164, 2, 322--344.

Digital Library

[34]

Mounir Maaref. 2007. Creating an opb ipif-based ip and using it in edk. http://www.xilinx.com/support/documentation/application_notes/xapp967.pdf.

[35]

Gabor Madl, Sudeep Pasricha, Luis Angel D. Bathen, Nikil Dutt, and Qiang Zhu. 2006. Formal performance evaluation of amba-based system-on-chip designs. In Proceedings of the 6^th ACM/IEEE International Conference on Embedded Software (EMSOFT'06). ACM Press, New York, 311--320.

Digital Library

[36]

Gabor Madl, Sudeep Pasricha, Nikil Dutt, and Sherif Abdelwahed. 2009. Cross-abstraction functional verification and performance analysis of chip multiprocessor designs. IEEE Trans. Industr. Informat. 5, 3, 241--256.

[37]

Carver Mead and Lynn Conway. 1980. Introduction to VLSI Systems. Addison-Wesley.

Digital Library

[38]

Robin Milner. 1989. Communication and Concurrency. Prentice-Hall.

Digital Library

[39]

Sanjiv Narayan and Daniel D. Gajski. 1995. Interfacing incompatible protocols using interface process generation. In Proceedings of the 32^nd Annual ACM/IEEE Design Automation Conference (DAC'95). 468--473.

Digital Library

[40]

Roberto Passerone, Luca de Alfaro, Thomas A. Henzinger, and Alberto L. Sangiovanni-Vincentelli. 2002. Convertibility verification and converter synthesis: Two faces of the same coin. In Proceedings of the IEEE/ACM International Conference on Computer Aided Design (ICCAD'02). 132--139.

Digital Library

[41]

Roberto Passerone, James A. Rowson, and Alberto Sangiovanni-Vincentelli. 1998. Automatic synthesis of interfaces between incompatible protocols. In Proceedings of the 35^th Annual Design Automation Conference (DAC'98). ACM Press, New York, 8--13.

Digital Library

[42]

Partha S. Roop, Alain Girault, Roopak Sinha, and Gregor Goessler. 2009. Specification enforcing refinement for convertibility verification. In Proceedings of the International Conference on Application of Concurrency to System Design (ACSD'09). IEEE Computer Society, 148--157.

Digital Library

[43]

Resve Saleh, Steve Wilton, Shahriar Mirabbasi, Alan Hu, Mark Greenstreet, Guy Lemieux, Partha Pratim Pande, Cristian Grecu, and Andre Ivanov. 2006. System-on-chip: Reuse and integration. Proc. IEEE 94, 6, 1050--1069.

[44]

Alberto Sangiovanni-Vincentelli and Grant Martin. 2001. Platform-based design and software design methodology for embedded systems. IEEE Des. Test Comput. 18, 6, 23--33.

Digital Library

[45]

Mike Santarini. 2011. Zynq-7000 epp sets stage for new era of innovations. Xcell J. 75, 8--13.

[46]

Roopak Sinha. 2009. Automated techniques for formal verification of socs. http://homepages.engineering.auckland.ac.nz/~roop/pub/phd/Roopak.pdf.

[47]

Roopak Sinha, Partha S. Roop, and Samik Basu. 2008. SoC design approach using convertibility verification. EURASIP J. Embedd. Syst. 2008, 1.

Digital Library

[48]

Roopak Sinha, Partha S. Roop, Samik Basu, and Zoran Salcic. 2009. Multi-clock soc design using protocol conversion. In Proceedings of the Design, Automation, and Test in Europe Conference (DATE'09). 123--128.

Digital Library

[49]

Roopak Sinha, Partha S. Roop, Zoran Salcic, and Samik Basu. 2012. Correct-by-construction multi-component soc design. In Proceedings of the Design, Automation and Test in Europe Conference (DATE'12). EDA Consortium, 647--652.

Digital Library

[50]

Wolfgang Thomas. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, Vol. B, Jan van Leeuwen, Ed., MIT Press, 133--191.

Digital Library

[51]

Massimo Tivoli, Pascal Fradet, Alain Girault, and Gregor Goessler. 2007. Adaptor synthesis for real-time components. In Proceedings of the 13^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07). 185--200.

Digital Library

[52]

Stavros Tripakis, Ben Lickly, Thomas A. Henzinger, and Edward A. Lee. 2009. On relational interfaces. In Proceedings of the International Conference on Embedded Software (EMSOFT'09). ACM Press, New York, 67--76.

Digital Library

[53]

Rob J. van Glabbeek. 1990. The Linear Time-Branching Time Spectrum. Springer.

[54]

Axel van Lamsweerde. 2001. Goal-oriented requirements engineering: A guided tour. In Proceedings of the 5^th IEEE International Symposium on Requirements Engineering (RE'01). 249--262.

Digital Library

[55]

Valeriy Vyatkin, James H. Christensen, and Jose L. Martinez Lastra. 2005. OOONEIDA: An open, object-oriented knowledge economy for intelligent industrial automation. IEEE Trans. Industr. Informat. 1, 1, 4--17.

[56]

Shigeru Watanabe, Kenshu Seto, Yuji Ishikawa, Satoshi Komatsu, and Masahiro Fujita. 2007. Protocol transducer synthesis using divide and conquer approach. In Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC'07). IEEE Computer Society, 280--285.

Digital Library

[57]

Xilinx. 2013. Support: IP documentation. http://www.xilinx.com/support/index.html/content/xilinx/en/supportNav/ip_documentation.html.

[58]

Hubert Zimmermann. 1980. OSI reference model--The iso model of architecture for open systems interconnection. IEEE Trans. Comm. 28, 4, 425--432.

Cited By

Dubinin VVyatkin VHanisch H(2015)Synthesis of Safety Controllers for Distributed Automation Systems on the Basis of Reverse Safe Net Condition/Event SystemsProceedings of the 2015 IEEE Trustcom/BigDataSE/ISPA - Volume 0310.1109/Trustcom.2015.646(287-292)Online publication date: 20-Aug-2015
https://dl.acm.org/doi/10.1109/Trustcom.2015.646
Castagnetti GPiccolo MVilla TYevtushenko NBrayton RMishchenko A(2015)Automated Synthesis of Protocol Converters with BALM-IIRevised Selected Papers of the SEFM 2015 Collocated Workshops on Software Engineering and Formal Methods - Volume 950910.1007/978-3-662-49224-6_23(281-296)Online publication date: 7-Sep-2015
https://dl.acm.org/doi/10.1007/978-3-662-49224-6_23

Index Terms

A Formal Approach to Incremental Converter Synthesis for System-on-Chip Design
1. Applied computing
  1. Physical sciences and engineering
    1. Engineering

Recommendations

Providing cost-effective on-chip network bandwidth in GPGPUs
ICCD '12: Proceedings of the 2012 IEEE 30th International Conference on Computer Design (ICCD 2012)

Network-on-chip (NoC) bandwidth has a significant impact on overall performance in throughput-oriented processors such as GPG-PUs. Although it has been commonly assumed that high NoC bandwidth can be provided through abundant on-chip wires, we show that ...
Automated bus generation for multiprocessor SoC design

The performance of a multiprocessor system heavily depends upon the efficiency of its bus architecture. This paper presents a methodology to generate a custom bus system for a multiprocessor system-on-a-chip (SoC). Our bus-synthesis tool, which we call ...
A monolithic buck DC-DC converter with on-chip PWM circuit

A monolithic CMOS voltage-mode, buck DC-DC converter with integrated power switches and new on-chip pulse-width modulation (PWM) technique of switching control is presented in this paper. The PWM scheme is constructed by a CMOS ring oscillator, which ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 20, Issue 1

November 2014

377 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/2690851

Editors:
Naehyuck Chang
Korea Advanced Institute of Science and Technology, Korea
,
David Z. Pan,
Yuan Xie

Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 18 November 2014

Accepted: 01 August 2014

Revised: 01 August 2014

Received: 01 March 2013

Published in TODAES Volume 20, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
143
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)2

Reflects downloads up to 04 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Dubinin VVyatkin VHanisch H(2015)Synthesis of Safety Controllers for Distributed Automation Systems on the Basis of Reverse Safe Net Condition/Event SystemsProceedings of the 2015 IEEE Trustcom/BigDataSE/ISPA - Volume 0310.1109/Trustcom.2015.646(287-292)Online publication date: 20-Aug-2015
https://dl.acm.org/doi/10.1109/Trustcom.2015.646
Castagnetti GPiccolo MVilla TYevtushenko NBrayton RMishchenko A(2015)Automated Synthesis of Protocol Converters with BALM-IIRevised Selected Papers of the SEFM 2015 Collocated Workshops on Software Engineering and Formal Methods - Volume 950910.1007/978-3-662-49224-6_23(281-296)Online publication date: 7-Sep-2015
https://dl.acm.org/doi/10.1007/978-3-662-49224-6_23

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents