SystemC Waiting-State Automata

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