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.