Parameterized Synthesis Case Study: AMBA AHB

TL;DR

This paper explores parameterized synthesis for the AMBA AHB protocol, demonstrating scalable implementation techniques for systems with many components, and achieving synthesis of a 14-state model in about an hour.

Contribution

It introduces property decompositional synthesis and direct encoding of GR(1) to improve parameterized synthesis for AMBA AHB.

Findings

Successfully synthesized a 14-state component model in about 1 hour.

Demonstrated scalable synthesis for arbitrarily many components in token rings.

Enhanced synthesis techniques with new optimization tricks.

Abstract

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.