Parameterized Synthesis Case Study: AMBA AHB (extended version)

TL;DR

This paper explores parameterized synthesis for AMBA AHB, demonstrating how to synthesize scalable implementations using token rings, property decomposition, and direct encoding, achieving efficient synthesis of small models.

Contribution

It introduces new techniques like property decompositional synthesis and direct encoding of GR(1) for parameterized synthesis in token rings, improving scalability and efficiency.

Findings

Synthesized a 14-state model in 30 minutes

Demonstrated scalable synthesis for arbitrarily many components

Applied new tricks to improve synthesis performance

Abstract

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.