Validation de modèles de systèmes sur puce en présence d’ordonnancements indéterministes et de temps imprécis@
Institution:
Grenoble INPGDisciplines:
Directors:
Abstract EN:
We study the validation by simulations of System-on-a-Chip models, written in SystemC-TLM. These models al used for the development of embedded software. Parallel entities of hardware are modeled by asynchronous processes, whose scheduling policy is non-deterministic in order to represent the physical parallelism faithfully. We have to cover the set of valid interleavings in addition to the set of data, since the result of a simulation may depend on the scheduling. We present an adaptation of dynamic partial order reduction to effectively cover the scheduling set, and an extension for timed models with bounded delays. The idea is to look at communications between processes, in order to guess whether a change in their order (as what would be produced by distinct scheduler choices) could affect the final state. This algorithm and its implementation return a complete schedulin and timing set, which guarantees the detection of aIl local errors and deadlocks for a fixed data set.
Abstract FR:
Nous étudions la validation par simulations de modèles SystemC- TLM de systèmes-sur-puce, servant au développement du logiciel embarqué. Les entités parallèles du matériel sont modélisées par des processus asynchrones, dont la politique d'ordonnancement est indéterministe afin de mieux représenter le parallélisme physique. Nous devons couvrir l'espace des ordonnancements en plus de celui des données, puisque le résultat d'une simulation peut dépendre de l'ordonnancement. Nous présentons une adaptation de la réduction d'ordre par dynamique pour couvrir efficacement l'espace des ordonnancements, ainsi qu'une extension pour les systèmes temporisés avec délais bornés. L'idée est d'observer les communications entre processus, pour générer dynamiquement de nouveaux entrelacements pertinents. Cet algorithme et le prototype réalisé retournent un ensemble d'ordonnancements et de jeux de durées, qui garantit la détection complète des erreurs locales et inter-blocages pour des données fixées.