# Parameterized Synthesis Case Study: AMBA AHB (extended version)

arXiv: https://arxiv.org/abs/1406.7608 · HTML: https://mlsanity.com/paper/1406.7608/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Jun 2014.

## Built on by (most cited first, 1 of 1)

- [Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control](https://mlsanity.com/paper/2406.07400/) (2024)

## Abstract (arXiv)

We revisit the AMBA AHB case study that has been used as a benchmark for several reactive syn- thesis 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 the model with 14 states in 30 minutes.