Exploiting timed transition relations in sequential cycle-based simulation of embedded systems

Embedded systems are increasingly important. They are currently implemented as a mix of hardware and software components, and they must satisfy strict real-time constraints. To achieve this, several counting devices are usually introduced in the system. As a result, embedded systems exhibit extremely deep state spaces, and standard analysis methods may be excessively expensive. More specifically, there is interest in very long sequences of states without `observable´ or `relevant´ external effects. A new symbolic approach to represent them is described which is based on timed transition relations. The methodology may be used for a variety of applications, from synthesis to verification and to simulation. The paper concentrates on simulation. In this field, starting from a register-transfer or gate-level description, a binary-decision-diagram-based model is extracted automatically which is capable of jumping in time, avoiding the simulation of internal events. Finally, a set of experimental results obtained using a state-of-the-art simulator is discussed