Parameterized Synthesis Case Study: AMBA AHB

Roderick Bloem
(Graz University of Technology, Austria)
Swen Jacobs
(Graz University of Technology, Austria)
Ayrat Khalimov
(Graz University of Technology, Austria)

We revisit the AMBA AHB case study that has been used as a benchmark for several reactive synthesis tools. Synthesizing AMBA AHB implementations that can serve a large number of masters is still a difficult problem. We demonstrate how to use parameterized synthesis in token rings to obtain an implementation for a component that serves a single master, and can be arranged in a ring of arbitrarily many components. We describe new tricks - property decompositional synthesis, and direct encoding of simple GR(1) - that together with previously described optimizations allowed us to synthesize a component model with 14 states in about 1 hour.

In Krishnendu Chatterjee, Rüdiger Ehlers and Susmit Jha: Proceedings 3rd Workshop on Synthesis (SYNT 2014), Vienna, Austria, July 23-24, 2014, Electronic Proceedings in Theoretical Computer Science 157, pp. 68–83.
Published: 18th July 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: