A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

We present a rewriting logic semantics in Maude of the ABEL hardware description language. Based on this semantics, and on Maude's underlying LTL model checker, we propose a scalable formal analysis framework and tool for hardware/software co-design. The analysis method is based on trace checking of finite system behaviors against LTL temporal logic formulas. The formal properties of the hardware, the embedded software, and the interactions between both can all be analyzed this way. We present two case studies illustrating our method and tool.