SystemC Waiting-State Automata

Delta-cycles are basic units of SystemC modeling and they are supposed to provide the guarantee of some critical properties about interactions between concurrent processes, like determinism and liveness, which is the basis for higher-level modeling and analysis. However, uncareful design may cause serious problems at the transaction level, which break the properties that we want to ensure at the level of delta-cycles. We propose a formal model based on SystemC waiting-state automata for verifying properties of SystemC models at the transaction level within a delta-cycle and show that this model conforms to the SystemC scheduler up to delta-cycles.