Roderick Bloem (Graz University of Technology, Austria) |
Swen Jacobs (Graz University of Technology, Austria) |
Ayrat Khalimov (Graz University of Technology, Austria) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.157.9 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |