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.
Author and article information
Project Everest, INRIA Sophia-Antipolis
2004, Route des Lucioles, BP 93, 06902 Sophia-Antipolis, France
CEA, LIST, Boîte 65, Gif-sur-Yvette, F-91191 France
UEI, ENSTA, 32 Bd Victor, 75739 Paris cedex 15, France