We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is then solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.
Associated Source Code here
Files with extension .nu are nuxmv command file. Files with extension .xmas are xmas language source files. File async.nuxmv is am asynchronous model. File sync.nuxmv is a synchronous model. File invarspec is the property being checked File invar cointains inductive invariants.