A Caltech Library Service

Revisiting the AMBA AHB bus case study

Filippidis, Ioannis and Murray, Richard M. (2015) Revisiting the AMBA AHB bus case study. California Institute of Technology , Pasadena, CA. (Unpublished)

[img] PDF - Draft Version
See Usage Policy.


Use this Persistent URL to link to this item:


This report describes a number of changes to the ARM AMBA bus case study from Bloem et al. that lead to significant reduction in synthesis time. In addition, it identifies the reason of blowup for the synthesized strategies in earlier studies as lack of binary decision diagram (BDD) reordering during strategy construction. Enabling dynamic BDD reordering with the group sifting algorithm, we synthesized strategies for as many as 18 masters, with both the original and revised specifications. This conclusion is based on detailed experimental measurements that show the changes of BDD sizes over time for the fixpoint and other variables during the nested fixed point computation, including the cumulative time spent on BDD reordering and the total number of BDD nodes. The measurements were obtained for eight different cases, allowing to compare the original with the revised specifications, with strategy reordering enabled or not, and conjoining the weak fairness guarantees or merging them into a single Büchi automaton. The revised specification proposed here is expressed using the open Promela language.

Item Type:Report or Paper (Technical Report)
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Contact Email
Additional Information:© 2015 by the authors. This work was supported in part by the TerraSwarm Research Center, one of six centers supported by the STARnet phase of the Focus Center Research Program (FCRP) a Semiconductor Research Corporation program sponsored by MARCO and DARPA.
Group:Control and Dynamical Systems Technical Reports
Funding AgencyGrant Number
TerraSwarm Research CenterUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Record Number:CaltechCDSTR:2015.004
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:57469
Deposited By: Ioannis Filippidis
Deposited On:13 May 2015 20:05
Last Modified:03 Oct 2019 08:25

Repository Staff Only: item control page