Parameterized Synthesis Case Study: AMBA AHB

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.

Conference version of arXiv:1406.7608. In Proceedings SYNT 2014, arXiv:1407.4937

References in corpus (5)

• LTL to Büchi Automata Translation: Fast and More Deterministic
• Parameterized Synthesis
• Parameterized Synthesis Case Study: AMBA AHB
• Parameterized Synthesis Case Study: AMBA AHB (extended version)
• Decidability Problems for Actor Systems

Cited by in corpus (7)

• Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
• Synthesizing a Lego Forklift Controller in GR(1): A Case Study
• Parameterized Synthesis Case Study: AMBA AHB
• Parameterized Synthesis Case Study: AMBA AHB (extended version)
• A multi-paradigm language for reactive synthesis
• The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
• Reactive Synthesis: Branching Logics and Parameterized Systems