Design and verification of pipelined circuits with Timed Petri Nets - Ecole Centrale de Nantes Accéder directement au contenu
Article Dans Une Revue Discrete Event Dynamic Systems Année : 2023

Design and verification of pipelined circuits with Timed Petri Nets

Résumé

A fundamental step in circuit design is the placement of pipeline stages, which can drastically increase the data throughput. Retiming allows optimizing the pipeline with regard to a criterion, for example the required number of registers. This article presents an extension of Timed Petri Net to model synchronous electronic circuits, in order to explore the design space of pipelines. The Timed Petri Nets “à la Ramchandani” with a maximal step firing rule, have notably been used for the modeling of electronic circuits. The RTPN extension, through the reset which model the pipeline stages, and through the delayable transitions which relax some temporal constraints, makes it possible to widen the design space of pipelined systems, and thus to deal with both the retiming and the verification. After a formal definition of this model, we present a method to explore pipelines verifying temporal properties. We apply our approach to a time-multiplexing property allowing the mutualization of operators while minimizing the number of registers.
Fichier principal
Vignette du fichier
main.pdf (467.45 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03952519 , version 1 (23-01-2023)

Identifiants

Citer

Rémi Parrot, Mikaël Briday, Olivier Roux. Design and verification of pipelined circuits with Timed Petri Nets. Discrete Event Dynamic Systems, 2023, 33, ⟨10.1007/s10626-022-00371-7⟩. ⟨hal-03952519⟩
18 Consultations
74 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More