Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published May 13, 2015 | Draft
Report Open

Revisiting the AMBA AHB bus case study

Abstract

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.

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.

Attached Files

Draft - amba_coda_0.pdf

Files

amba_coda_0.pdf
Files (5.0 MB)
Name Size Download all
md5:88a51fed2b065d0321456a88190e1f9b
5.0 MB Preview Download

Additional details

Created:
August 20, 2023
Modified:
October 23, 2023