Exploiting timed transition relations in sequential cycle-based simulationof 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 usual ly introduced in the system. As a result, embedded systems exhibit extremel y deep state spaces, and standard analysis methods may be excessively expen sive. More specifically, there is interest in very long sequences of states without 'observable or 'relevant' external effects. A new symbolic approac h to represent them is described which is based on timed transition relatio ns. The methodology may be used for a variety of applications, from synthes is 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. Fi nally, a set of experimental results obtained using a state-of-the-art simu lator is discussed.