Parameterized Synthesis Case Study: AMBA AHB (extended version)
This addresses a difficult problem in reactive synthesis for hardware design, but it is incremental as it builds on existing optimizations with new tricks.
The paper tackled the challenge of synthesizing AMBA AHB implementations for many masters by using parameterized synthesis in token rings, resulting in a model with 14 states synthesized in 30 minutes.
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.