Compositional Reactive Semantics of SystemC and Verification with RuleBase

We present a behavioral semantics of SystemC that succinctly captures its reactive features, clock and time references, macro- and micro-time model, and allows the specification of a network of synchronous and asynchronous components Communicating through either high-level transactions or low-level signal and event communications. The proposed semantic framework demonstrates the anomalies introduced by the simulation kernel, in spite of the macro- and micro-time scales. The framework further relates the simulation and logical correctness and provides a technique for scaling up the verification while keeping the correctness intact. Furthermore, we translate SystemC components to RuleBase using Our semantic characterization that pen-nits testing and verification of heterogenous designs. We illustrate the verification of a Central Locking System (CLS) designed in SystemC.