Design and verification of pipelined circuits with Timed Petri Nets

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 "a 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.