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.
Cite
@article{arxiv.1406.7608,
title = {Parameterized Synthesis Case Study: AMBA AHB (extended version)},
author = {Roderick Bloem and Swen Jacobs and Ayrat Khalimov},
journal= {arXiv preprint arXiv:1406.7608},
year = {2016}
}
Comments
Moved to appendix some not very important proofs. To section 'optimizations: added the model for 0-process. Extended version of the paper submitted to SYNT 2014