Parameterized Synthesis Case Study: AMBA AHB

被引：10

作者：

Bloem., Roderick ^{[1
]}

Jacobs, Swen ^{[1
]}

Khalimov, Ayrat ^{[1
]}

机构：

[1] Graz Univ Technol, Graz, Austria

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2014年 / 157期

基金：

奥地利科学基金会;

关键词：

D O I：

10.4204/EPTCS.157.9

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：68 / 83

页数：16

共 17 条

[1]

Aminof B, 2014, LECT NOTES COMPUT SC, V8318, P262, DOI 10.1007/978-3-642-54013-4_15

[2]

ARM Ltd, 1999, AMBA SPEC REV 2

[3]

Babiak T, 2012, LECT NOTES COMPUT SC, V7214, P95, DOI 10.1007/978-3-642-28756-5_8

[4] Synthesis of Reactive(1) designs [J].

Bloem, Roderick ;

Jobstmann, Barbara ;

Piterman, Nir ;

Pnueli, Amir ;

Sa'ar, Yaniv .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (03) :911-938

[5]

Bloem R, 2010, LECT NOTES COMPUT SC, V6174, P425, DOI 10.1007/978-3-642-14295-6_37

[6]

Bloem Roderick, 2014, ARXIV14067608

[7] Z3: An efficient SMT solver [J].

de Moura, Leonardo ;

Bjorner, Nikolaj .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 :337-340

[8]

Emerson E. A., 2003, INT J FOUND COMPUT S, V14, P527

[9] Bounded synthesis [J].

Finkbeiner B. ;

Schewe S. .

International Journal on Software Tools for Technology Transfer, 2013, 15 (5-6) :519-539

[10]

Finkbeiner B, 2012, LECT NOTES COMPUT SC, V7148, P219, DOI 10.1007/978-3-642-27940-9_15

← 1 2 →