Rémi Parrot
email: remi.parrot@ec-nantes.fr

Mikaël Briday
email: mikael.briday@ec-nantes.fr

Olivier H Roux
email: olivier-h.roux@ec-nantes.fr

Design and verication of pipelined circuits with Timed Petri Net *

Keywords: pipeline optimization, model checking, Timed Petri Net, resource sharing, time-multiplexing, synchronous circuit

A fundamental step in circuit design is the placement of

pipeline stages, which can drastically increase the data throughput. The retiming allows optimizing the pipeline with regard to a criterion, for example the required number of registers. The Timed Petri Nets à la Ramchandani with a maximal step ring rule, have been notably 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 possible to widen the design space of pipelined systems, and thus to deal with both the retiming and the verication.

After a formal denition 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.

Design and verication of pipelined circuits with TPN 1 Introduction Timing constraints are a major problem in the design of synchronous logical circuits. To meet these constraints the pipeline is often inevitable, it allows increasing the operating frequency and thus the throughput. The circuit composed of atomic operators is sliced in several steps called stages. This slicing, physically implemented with memories (ip-ops), allows the concurrent execution of stages and the synchronization of their inputs/outputs. The automatic generation of pipeline, i.e. the ecient placement of ip-ops (1 bit registers), aims not only at ensuring a target frequency but also minimizing the resources consumed by the pipeline.

Automatic pipeline generation

The automatic pipeline generation was initially formalized by Leiserson and Saxe in [START_REF] Leiserson | Retiming synchronous circuitry[END_REF], using a model of graph. Their method is based on the retiming, i.e. moving registers in the circuit without altering the behavior. Thanks to the retiming they are able to build a pipeline guaranteeing a minimal throughput, while minimizing the resources consumed by the pipeline registers [START_REF] Leiserson | Retiming synchronous circuitry[END_REF]. They reformulate the problem with a minimum cost ow problem. But it turned out to be inecient for large circuits, and therefore has been replaced in [START_REF] Hurst | Fast minimum-register retiming via binary maximum-ow[END_REF] by a reformulation into an iterative maximal ow problem. This solution is implemented at the logical synthesis level in the ABC tool [START_REF] Logic | ABC: A system for sequential synthesis and verication[END_REF], which is to our knowledge the current state of the art. However, these algorithms are in practice hard to implement, and are mainly used by FPGA vendor tools at the logical synthesis level.

We propose a new approach able to solve this same problem, but also to verify by model checking temporal constraints. Moreover, this model, which preserves the structure of the circuit, is quite suitable for optimizations beyond the pipeline, such as the sharing of circuit parts.

Circuit design with Petri Nets

The authors of [START_REF] Leiserson | Retiming synchronous circuitry[END_REF] introduced an abstraction of circuit with a weighted directed graph. The intuition behind this model is actually a marked graph, which is a subclass of Petri Net (PN) where every place has exactly one input arc and one output arc. Because of their concurrent nature, the PNs have been widely employed to analyze and optimize temporal properties of synchronous and asynchronous circuits: [START_REF] Bustov | A general model for performance optimization of sequential systems[END_REF][START_REF] Campos | Properties and performance bounds for timed marked graphs[END_REF][START_REF] Najibi | Slack matching mode-based asynchronous circuits for average-case performance[END_REF][START_REF] Kim | Pipeline optimization for asynchronous circuits: complexity analysis and an ecient optimal algorithm[END_REF].

They proved to be very ecient for latency insensitive systems. Bustov et al. [START_REF] Bustov | A general model for performance optimization of sequential systems[END_REF] extended the works of Leiserson and Saxe on latency insensitive systems, by combining retiming with recycling, i.e. insertion of bubbles (registers with no informative value), in order to reduce the total number of registers while ensuring a minimal throughput. More recently, Josipovic et al. [START_REF] Josipovi¢ | Buer placement and sizing for high-performance dataow circuits[END_REF] proposed a temporal optimization of circuits generated from an HLS (High Level Synthesis) description with control ow structures, by applying the approach of [START_REF] Bustov | A general model for performance optimization of sequential systems[END_REF] on extracted sub-circuits.

Springer Nature 2021 L A T E X template Design and verication of pipelined circuits with TPN

All those works share the same solving method: deduce temporal constraints from the structure of the PN, and reformulate with a linear optimization problem. In contrast, our approach makes use of the semantics of PNs and synthesizes directly the pipeline from the states of the model. The explicit exploration of the states oers a simple way to verify logical and temporal properties on the resulting pipelined circuit.

Model-Checking

The model-checking originates in the verication of electronic circuits [START_REF] Kern | Formal verication in hardware design: A survey[END_REF]. The expressive power of formal models like PN, allows modeling both the circuit and its environment, thus to verify a complete system. We can, for example, verify an FPGA working together with a microcontroler, and all connected to a set of sensors and actuators.

The temporal logics were rst introduced by Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF] as specication languages to describe the behavior of sequential and concurrent systems. The TCTL [START_REF] Alur | Model-checking in dense real-time[END_REF] and weighted CTL [START_REF] Bouyer | Model checking one-clock priced timed automata[END_REF] logics extend respectively the temporal tree logic CTL, to time and to cost constraints.

We propose to illustrate a usage of those temporal logics for the modelchecking of circuits with the example of time-multiplexing. It is a technique of resources sharing using time to sequence the access to a resource. This kind of property can be easily expressed and veried on a PN model.

Time-Multiplexing

Time-multiplexing is especially interesting for applications with a low throughput with respect to the clock frequency. Such applications include, for example, signal processing applications implemented on FPGA, which require a very low sampling rate compared to the FPGA frequency (e.g. a 1 MHz signal processing algorithm onto a 100 MHz FPGA). In this kind of context, it is benecial to implement only once, parts of the circuit which are used several times, and to schedule their access with the pipeline.

Many works have been carried out in this domain, notably through a problem called modulo scheduling. This problem aims for a minimal latency in a time-multiplexed circuit, given limited available resources (arithmetic or logic operators). The authors of [START_REF] Sittel | Ilp-based modulo scheduling and binding for register minimization[END_REF] proposed an ILP (Integer Linear Programming) formulation which combines scheduling constraints, bounds on available resources, minimization of needed registers, and mutualization of registers when it is possible. More recently, a two steps process was demonstrated by [START_REF] Sittel | Isomorphic subgraph-based problem reduction for resource minimal modulo scheduling[END_REF]: rst the shareable congurations are detected, then each conguration is scheduled. This approach called folding allows sharing portions of the circuit in contrast with the previous approaches which were only able to share operators one by one.

Design and verication of pipelined circuits with TPN

Putting it all together

As part of the work with Renault, the automotive company, we aim at optimizing VHDL synthesis for an FPGA target, from a Matlab/Simulink project.

Specically, the goal is to implement a synchronous circuit with a minimum resource consumption, both for logical units and ip-ops, while ensuring that the whole computation is done in a limited time-frame (the sampling period).

A tool is under heavy development, in order to propose a complete chain for the hardware implementation of control laws directly in FPGA. This section briey introduces the dierent parts considered in this tool.

The compiler is classically organized around an internal representation, independent of both the input (Simulink) and output (VHDL) representations. This internal model serves as a pivot for all the tools, with dierent optimizations. The general architecture of the tool is depicted in Figure 1. Eventually, the goal is to make this pass semi-automatic, using both interval arithmetic and ane arithmetic [START_REF] Lee | Accuracy-guaranteed bit-width optimization[END_REF], and recent work for example for linear looped systems [START_REF] Hilaire | Error analysis methods for the xed-point implementation of linear systems[END_REF].

Internal Model

The evaluation of operator delays is required in modeling with Petri nets extensions dened in the paper. The level of abstraction of the operators in Simulink does not allow to calculate precisely these delays. The approach used, as for the FloPoco tool [START_REF] De | Designing custom arithmetic data paths with FloPoCo[END_REF], is to synthesize each operator to determine its critical path. The delay of each evaluated operator is then recorded in a database because this synthesis is computer intensive. This pass is automated through a script and is based on an experimental-only approach. The delay of the operators will necessarily vary during the synthesis of the nal project (branching, internal optimizations, interconnections, . . . ). It is only possible to validate that all deadlines are met after the nal synthesis.

The last pass (in green in the gure) is the one that is presented in this article and is a synthesis and extension of the articles [START_REF] Parrot | Pipeline Optimization using a Cost Extension of Timed Petri Nets[END_REF][START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF], which introduce the model Timed Petri Net with reset and delayable transitions (RTPN in short) and present its usage for pipeline synthesis. Here, the focus is on the addition of temporal logic constraints to the generation of pipelines.

Outline

We rst present in the Section 2 a semantics of Timed Petri Nets à la Ramchandani [START_REF] Ramchandani | Analysis of asynchronous concurrent systems by timed Petri nets[END_REF] with an atomic ring rule using maximal steps, i.e. without the three phases ring. Then, in the Section 3, we present an extension of Timed Petri Nets (proposed in [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF]) closer to the real synchronous circuits, which embeds the impacts of registers on the delay of the circuit with a particular reset operation, and which allows relaxing some temporal constraints with delayable transitions.

Thanks to this accurate model of pipelined synchronous circuits, we present in the Section 4 a design space exploration guided by a cost which stands for the number of needed registers (proposed in [START_REF] Parrot | Pipeline Optimization using a Cost Extension of Timed Petri Nets[END_REF]). We extend this approach in the Section 5 in order to build optimized pipelines (in terms of number of registers), while guaranteeing that a set of properties are veried by the synthesized circuit. We apply this approach to the time-multiplexing problem.

A synchronous model for the pipeline

The use of deterministic time in PN was rst introduced by Ramchandani [START_REF] Ramchandani | Analysis of asynchronous concurrent systems by timed Petri nets[END_REF],

which led to a model called Timed Petri Net. Each transition is associated with a delay, representing the fact that actions take time to complete.

N and R ≥0 are respectively the sets of integer and non-negative real numbers. For vectors of size n, the usual operators +, -, <, ≤, >, ≥ and = are used on vectors of N n and R n ≥0 and are the point-wise extensions of their counterparts in N and R ≥0 . Let 0 be the null vector of size n.

The three-phases ring semantics

Ramchandani's semantics is a three-phases ring semantic: delete the input tokens of the transition (consumption), wait until the ring time is reached (delay) and create the output tokens of the transition (production). Once initiated, this ring process cannot be interrupted or stopped. The consumption Design and verication of pipelined circuits with TPN phase can therefore be seen as a reservation (in particular in case of conict).

Moreover, the transitions in the ring process are synchronized to a global clock. He furthermore prohibits zero time ring, which prevents the same transition from being red twice when other transitions are in conict.

Popova proposed a semantic based on the same three-phases ring, but selecting beforehand a maximal step of transitions to re in the same atomic action [START_REF] Popova-Zeugmann | Time and Petri Nets[END_REF]. In other words, instead of being reserved one after the other, the transitions are selected and then reserved all at the same time (consumption phase).

The maximal-step ring semantics

Classically the semantics of (timeless) PN is the interleaving semantics, in which transitions are red one after the other. In the maximal-step semantics, a maximal set of reable transitions is selected and are then red all at once. In practice the maximal-step semantics avoids the interleaving, which is interesting for the modeling of synchronous systems. It imposes more constraints than the interleaving semantics, and thus increases the expressiveness and eliminates reachable markings.

Popova shows how a counter machine can be encoded and simulated by timeless PN with maximal-step ring, which then also applies to TPNs [START_REF] Popova-Zeugmann | Time and Petri Nets[END_REF]. In particular, she shows the modeling of the so-called zero-test, which is recalled in Figure 2a. It means that Timeless as Timed PNs ring in maximal-step are Turing equivalent.

An atomic semantics for TPNs

We consider a TPNs atomic semantics [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF] without any reservation: waiting is done while keeping the tokens in their place, then when at least one transition is reable we select the maximal step and re (consumption and production) all the transitions in one atomic action. The maximal step contains enabled transitions which have been enabled for a period of time equal to their delays.

Informally, a clock and a delay are associated with each transition of the Net. The clock measures the time elapsed since the transition has been enabled and the delay is interpreted as a ring condition: the transition may and must re if the value of its clock is equal to the delay. Formally: Denition 1 (TPN). A TPN is a tuple (P, T, • (.), (.) • , δ, M 0 ) dened by: P = {p 1 , p 2 , . . . , p m } is a non-empty set of places, T = {t 1 , t 2 , . . . , t n } is a non-empty set of transitions, • (.) : T → N P is the backward incidence function, (.) • : T → N P is the forward incidence function, M 0 ∈ N P is the initial marking of the Petri Net, δ : T → N is the function giving the ring times (delays) of transitions.

A marking M is an element of N P such that ∀p ∈ P , M (p) is the number of tokens in place p. A marking M enables a transition t ∈ T

if: M ≥ • t. The set of transitions enabled by a marking M is enab (M ) = {t ∈ T | M ≥ • t}. A
transition is reable if it is enabled and its clock has reached its delay.

Fireable transitions are red simultaneously according to the maximal-step ring rule. For marked graph where every place has one incoming arc, and one outgoing arc, there can not be any conict and the ring of a transition cannot disable another transition. In the general case, there can be conict and, from a given state, there can be several maximal steps τ .

From a marking M , the simultaneous ring of a set τ of transitions leads to a marking

M = M + Σ t∈τ t • -• t .
A transition t is said to be newly enabled by the ring of a set of transitions

τ if M + Σ t∈τ t • -• t enables t and (M -Σ t∈τ • t) did not enable t . If t
remains enabled after its ring then t is newly enabled. The set of transitions newly enabled by a set of transitions τ for a marking M is noted ↑ enab (M, τ ).

A state is a pair (M, v) where M is a marking and v ∈ R T ≥0 is a time valuation of the system (i.e. the value of the clocks). v(t) is the time elapsed since the transition t ∈ T has been newly enabled. 0 is the valuation assigning 0 to every transition.

Denition 2 (Maximal Step). Let q = (M, v) be a state of the TPN

(P, T, • (.), (.) • , δ, M 0 ), τ ⊆ T is a maximal step from q i: 1. ∀t ∈ τ, v(t) = δ(t) 2. t∈τ • t ≤ M 3. ∀t ∈ T, (v(t ) = δ(t ) and • t ≤ M and t ∈ τ ) ⇒ t∈τ • t + • t ≤ M
The set of maximal steps from q is noted maxStep(q)

The rst condition ensures that the transitions are ready to re, i.e. the clocks are equal to the delays. The second condition ensures that the transition are reable, i.e. enabled and not in conict with another transition of τ . The third condition disallows the existence of a proper superset of τ which fullls the previous two conditions.

The semantics of TPN is dened as a Timed Transition System (TTS).

Waiting in a marking is a delay transition of the TTS and ring a maximal step is a discrete transition of the TTS. Denition 3 (Semantics of a TPN). The semantics of a TPN is dened by the Timed Transition System S = (Q, q 0 , →):

Q = N P × R T ≥0 is the set of states, q 0 = (M 0 , 0) is the initial state, →∈ Q × (R ≥0 ∪ 2 T ) × Q is the
transition relation including a discrete transition and a delay transition.

• The delay transition is dened ∀d ∈ R ≥0 by:

(M, v) d -→ (M, v ) iff ∀t ∈ enab (M ) , v (t) = v(t) + d and v (t) ≤ δ(t)
• The discrete transition is dened ∀τ ∈ maxStep (M, v) by: Design and verication of pipelined circuits with TPN

(M, v) τ -→ (M , v ) iff      M = M + t∈τ t • -• t v (t) = 0 if t ∈↑ enab (M, τ ) or t ∈ enab (M ) v(t) otherwise
A run in a TPN is a sequence q 0 α1 -→ q 1 α2 -→ . . . , such that for all i, q i αi+1 ---→ q i+1 is a transition in the semantics.

In the absence of conict, the atomic semantics of Denition 3 is equivalent to the three-phases one of Ramchandani (extended with zero ring delay [START_REF] Popova-Zeugmann | Time and Petri Nets[END_REF]): it exists only one run, no indeterminism. In case of conict, it is possible to construct the three-phases ring in our semantics: just add a zero time transition before each transition, in order to simulate the reservation action [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF].

Zero-test and model of the pipeline

Thanks to the maximal step ring, a TPN represented on Figure 2a can perform the zero-test. After ring the transition start, the transitions test and cancel are red simultaneously if and only if the place p is marked. The next step will contain the transition is_zero i p wasn't marked, which leads to a token in p zero . We will use this test several times in the following, thus we will replace it by the graphical shortcut of Figure 2b for convenience.

Using this zero-test, it is directly possible to model the dataow of a pipeline. The TPN of Figure 3 models a D ip-op, which is used for the synchronization of a signal between two pipeline stages. The marking of the place Q i (or D i ) represents the presence of data (not its truth value).

On the left of the zero-test, the generator models the oscillator by adding a token in the place clock every N time unit. When the place clock is marked, the zero-test will put a token in Q i (output) only if the place D i (input) is marked. We thus model a D ip-op (copy the input signal D i to the output Q i on a rising edge of the clock), which synchronizes the dataow with clock.

Model-checking on pipeline is then possible. However, this model only allows the study of one pipeline (one placement of the D ip-ops in the circuit) at a time.

TPN with reset and delayable transitions

We have proposed in [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF] an extension of TPN where transitions are separated in two groups: asap transitions (non-delayable) must re as soon as possible, as in the Denition 1, and delayable transitions can re when their clock reaches their delay, or when their clock exceeds their delay and they are associated with another transition whose clock just reaches its delay. In addition, the clocks can be resetted (the corresponding action is called reset) and the delay between two consecutive resets is xed by an interval I reset . dened by:

(P, T, • (.), (.) The maximal step is then maximal only with regard to the asap transitions:

Denition 5 (Maximal Step w.r.t. T D ). Let q = (M, v) be a state of N . τ ⊆ T is a maximal step with regard to T D from q i:

1. ∀t ∈ τ, v(t) ≥ δ(t) 2. ∃t ∈ τ s.t. v(t) = δ(t) 3. t∈τ • t ≤ M 4. ∀t ∈ T \ T D , (v(t ) = δ(t ) and • t ≤ M and t ∈ τ ) ⇒ t∈τ • t + • t ≤ M
The set of maximal steps w.r.t.

T D from q is noted maxStep \T D (q). A state is now a pair (M, v) such that v ∈ R T ∪{reset} ≥0
is extended with a clock value for reset, evaluating the time elapsed since the last reset. The reset action resets all clocks of the net. It is possible only when its clock is in the reset interval v(reset) ∈ I reset .

The semantics of a RTPN is dened as a Timed Transition System (TTS).

Waiting in a marking is a delay transition of the TTS, and ring a maximal step or the reset are discrete transitions of the TTS. Denition 6 (Semantics of a RTPN). The semantics of a RTPN N is dened by the Timed Transition System S N = (Q, q 0 , →) with

Q = N P × R T ∪{reset} ≥0
is the set of states; q 0 = (M 0 , 0) is the initial state; and →∈ Q × (R ≥0 ∪ 2 T ∪ {reset}) × Q is the transition relation including a discrete transition and a delay transition:

The delay transition is dened ∀d ∈ R ≥0 by:

(M, v) d -→ (M, v ) iff      ∀t ∈ enab (M ) ∪ {reset}, v (t) = v(t) + d v (reset) ≤ I reset ∀t ∈ enab (M ) \ T D , v (t) ≤ δ(t)
The discrete transition is dened by:

∀τ ∈ maxStep \T D (M, v) , (M, v) τ -→ (M , v ) iff      M = M + Σ t∈τ t • -• t v (t) = 0 if t ∈↑ enab (M, τ ) or t ∈ enab (M ) v(t) otherwise (M, v) {reset} -----→ (M, v ) iff v(reset) ∈ I reset v = 0
Denition 7 (Runs). Let N be a RTPN and S N its semantics. A run of N from q is nite or innite sequence ρ = q d1 -→ q d1 τ1 -→ q τ1 . . . dn -→ q dn τn -→ q τn of alternating delay d i (possibly null) and discrete transition τ i where either τ i ⊆ T or τ i = {reset}. For all run ρ, it exists a discrete run ρ d = q τ1 -→ q τ1 . . . τn -→ q τn , in which only the discrete transitions are present.

Example

Let us consider the RTPN depicted in Figure 4a. Figure 4b shows a part of its state graph, restricted to the rst occurrence of a reset. States after a reset are framed in cyan. For more convenience, the markings are represented as the set of marked places. The initial state of the net is the state q 0 in the state graph.

Note that the transition t 0 being delayable, it can re when it reaches its delay (edge between q 1 and q 2 ), or together with t 3 (edge between q 8 and q 9 ).

Finally, it should be noted that not all the possible runs are represented here.

It is for example possible to wait 7 time units from q 0 and then do a reset.

Actually it exists innitely many runs, as a result of the density of time.

Properties of RTPNs

Symbolic state

The RTPN semantics is a transition system in which each state consists of a marking and a valuation of the clocks. Note that there is (because we only consider bounded nets) only a nite number of markings, but there is an uncountable quantity of valuations because of the density of time (particularly for the states from which a reset is possible). For example, there is innitely many states between q 8 and q 11 (in the Figure 4b). These states correspond to the wait between 6 and 9 from the state q 0 which can be abstracted by v(t 0 ) = v(t 3 ) = v(reset) ∈ [START_REF] Bustov | A general model for performance optimization of sequential systems[END_REF][START_REF] Hilaire | Error analysis methods for the xed-point implementation of linear systems[END_REF]. The state space can then easily be abstracted by a nite set of symbolic states. Denition 8 (Symbolic state). A symbolic state is a pair (M, Z) where M is a marking, and the zone Z is a set of valuation v of T ∪ {reset} dened by the conjunction of:

rectangular constraints: (v(x) ∼ c) where x ∈ T ∪ {reset}, ∼∈ {≤, =, ≥} and c ∈ N, diagonal constraints: (v(reset) -v(t) = c) where t ∈ enab (M ) and c ∈ N.
It is then possible to build a symbolic state graph as dened in [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF] illustrated in the example Figure 5. Compared to the part of state graph of Figure 4b, we can see that some states have been grouped into a single symbolic state.

It is interesting to note that the zones have a particular shape: the diagonal constraints are equalities and compare all the clocks with v(reset). Thus, by simply setting a value of v(reset) we can choose a point of the zone. The discrete actions (other than reset) are then only done on integer points of the space and the symbolic state space preserve the language in addition to the Design and verication of pipelined circuits with TPN reachability. Based on this abstraction it is possible to build a single clock automata that recognized the same language, as presented in [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF].

I reset = [6, 10] (a) Example of RTPN N {p0, p3} v(t0) = 0 v(t3) = 0 v(reset) = 0 {p0, p3} v(t0) = 5 v(t3) = 5 v(reset) = 5 {p1, p2, p3} v(t1) = 0 v(t2) = 0 v(t3) = 5 v(reset) = 5 {p1, p2, p3} v(t1) = 2 v(t2) = 2 v(t3) = 7 v(reset) = 7 {p1, p5} v(t1) = 2 v(reset) = 7 {p1, p5} v(t1) = 4 v(reset) = 9 {p4, p5} v(reset) = 9 {p4, p5} v(reset) = 0 {p0, p3} v(t0) = 9 v(t3) = 9 v(reset) = 9 {p1, p2, p6} v(t1) = 0 v(reset) = 9 {p1, p2, p6} v(t1) = 0 v(reset) = 0 {p0, p3} v(t0) = 6 v(t3) = 6 v(reset) = 6 {p0} v(t0) = 9 v(reset) = 9 {p0} v(t0) = 0 v(reset) = 0 {p1, p2, p3} v(t1) = 1 v(t2) = 1 v(t3) = 6 v(reset) = 6 {p1, p2, p3} v(t1) = 0 v(t2) = 0 v(t3) = 0 v(reset) = 0 {p1, p5} v(t1) = 0 v(reset) = 0 5 {t0} 2
An abstraction preserving the branching is readily accessible. Simply split the zone when a transition is no more reable. For example the state s a of Figure 5 becomes the states presented in Figure 6.

Without going into details on symbolic state graph, it should be noted that only few discrete runs are sucient to describe all the behaviors. We will then only represent the relevant states in the following state graphs.

Decidability and complexity

Timeless PNs, with the maximal step ring, are as expressive as a Turing

Machine and are a subclass of RTPN for whom the reachability problem is then

{p0, p3} 0 ≤ v(t0) 0 ≤ v(t3) ≤ 9 0 ≤ v(reset) ≤ 10 v(reset) -v(t0) = 0 v(reset) -v(t3) = 0 {p1, p2, p3} 0 ≤ v(t1) ≤ 4 0 ≤ v(t2) ≤ 2 5 ≤ v(t3) ≤ 9 5 ≤ v(reset) ≤ 10 v(reset) -v(t1) = 5 v(reset) -v(t2) = 5 v(reset) -v(t3) = 0 {p1, p2, p6} 0 ≤ v(t1) ≤ 4 9 ≤ v(reset) ≤ 10 v(reset) -v(t1) = 9 {p0, p6} 9 ≤ v(t0) 9 ≤ v(reset) ≤ 10 v(reset) -v(t0) = 0 {p1, p2, p3} 0 ≤ v(t1) ≤ 4 0 ≤ v(t2) ≤ 2 0 ≤ v(t3) ≤ 9 0 ≤ v(reset) ≤ 10 v(reset) -v(t1) = 0 v(reset) -v(t2) = 0 v(reset) -v(t3) = 0 {p1, p5} 2 ≤ v(t1) ≤ 4 7 ≤ v(reset) ≤ 10 v(reset) -v(t1) = 5 {p1, p2, p6} 0 ≤ v(t1) ≤ 4 0 ≤ v(reset) ≤ 10 v(reset) -v(t1) = 0 {p0, p6} 0 ≤ v(t0) 0 ≤ v(reset) ≤ 10 v(reset) -v(t0) = 0 {p1, p5} 0 ≤ v(t1) ≤ 4 0 ≤ v(reset) ≤ 10 v(reset) -v(t1) = 0 {p4, p5} 9 ≤ v(reset) ≤ 10 {p4, p5} 0 ≤ v(reset) ≤ 10 {reset} { t 0 } {t 0 , t 3 } { t 3 } { r e s e t}
{p0, p3} 0 ≤ v(t0) ≤ 5 0 ≤ v(t3) ≤ 9 0 ≤ v(reset) ≤ 10 v(reset) -v(t0) = 0 v(reset) -v(t3) = 0 {p0, p3} 5 ≤ v(t0) 5 ≤ v(t3) ≤ 9 5 ≤ v(reset) ≤ 10 v(reset) -v(t0) = 0 v(reset) -v(t3) = 0 { t 0 } 5 {reset} {t0 , t3 } {t 3 } s 1 a s 2 a
Fig. 6: Abstraction preserving the branching of state s a of Figure 5 also not decidable. But if we consider bounded nets, we obtain the following results:

Theorem 1. Reachability and TCTL model checking for a bounded TPN, with or without reset and delayable transitions, are PSPACE-complete.

Proof. PSPACE-hardness comes from the PSPACE-completness of the reachability problem for a safe timeless PN with the classical interleaving semantics, which is a subclass of bounded TPN. Then the PSPACE-completness is obtained by applying the same procedure as in [START_REF] Alur | Model-checking in dense real-time[END_REF][START_REF] Boucheneb | TCTL model checking of time Petri nets[END_REF] by checking TCTL formulae with an inductive algorithm for region graph exploration, which is polynomial in space.

Theorem 2. For bounded RTPN, the universality and language inclusion problems are decidable for nite timed words.

Proof. It is a consequence of the translation preserving the timed bisimulation proposed in [START_REF] Parrot | Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design[END_REF] of bounded RTPNs to one clock timed automata, for which these problems are decidable [START_REF] Parosh | Universality analysis for one-clock timed automata[END_REF][START_REF] Ouaknine | On the language inclusion problem for timed automata: closing a decidability gap[END_REF].

Design and verication of pipelined circuits with TPN 4 Pipeline synthesis

The model presented in Section 3 can accurately represent pipelined synchronous circuits. The following will demonstrate how to use this model to build an optimized pipeline which ensures a minimal frequency while minimizing the required registers (and thus the material resource consumed).

In this modeling, transitions represent the operators and places represent the connections of the circuit. The PN is actually a Marked Graph, and there is no conict. However, the state space still has an exponential size regarding the size of the RTPN. Some features are then used to limit the exploration according to an optimization objective.

The goal is to build the pipeline which minimizes the total number of ipop (1 bit register). The RTPN model is then extended with a cost representing the number of ip-ops of a given pipeline. Note that the considered circuits are nite and with unfolded loops, so we focus on nite runs of RTPN: the accumulation of an increasing cost will not aect the termination.

This pipeline building problem which minimizes the number of registers while ensuring a minimal frequency was already solved by [START_REF] Leiserson | Retiming synchronous circuitry[END_REF]. However, the proposed solution cannot be easily extended with additional constraints on the pipeline. The originality of the approach lies in the possibility to append a set of properties to check, to the pipeline synthesis. Those properties can, for example, permit sharing a portion of the circuit between several pipeline stages. The synthesis of pipeline allowing resource sharing will be addressed afterwards in the Section 5.

RTPN with cost

The RTPN is extended with a cost on each place, and a marking cost function.

Denition 9 (CRTPN).

A CRTPN is a tuple (N , C, ω) where N = (P, T, T D , • (.), (.) • , δ, I reset , M 0 ) is a RTPN and C : P → N is the cost assigned to each place; ω : N P → N is the marking cost function (recall that a marking is M ∈ N P ).

A classical marking cost function is ω(M ) = p∈P M (p) • C(p) which is the sum of the marking of each place weighted by its cost. This function is not necessarily linear, as we will see for the model of branching points.

Denition 10 (Cost of a run). The cost Ω(ρ) of a run ρ is the accumulated marking cost of the states after each reset in the run, starting by the cost of the initial marking.

It is dened inductively on a run ρ n = ρ n-1 αn --→ q n , with α n ∈ R ≥0 ∪ 2 T ∪ {reset} and q n = (M n , v n ) by:

Ω(q 0 ) = ω(M 0 ) Ω(ρ n ) = Ω(ρ n-1 ) + ω(M n ) if α n = {reset} Ω(ρ n-1 ) otherwise 4.

Modeling the circuit

A set of rules to model a circuit with a CRTPN is dened in this section. Figure 7 shows an example of circuit, with the operators op i connected by signals s i . The size of each signal is noted between parenthesis (in green).

The propagation delay of each operator is noted under it (in red). Lastly the pipeline's registers are represented by (blue) rectangles on the edges. Design and verication of pipelined circuits with TPN T = T Op T B with T Op = φv(Op) and T B = φv(B). rule 3: If s ∈ E is an input signal of v ∈ V , then • t(p) = 1 with t = φv(v) and p = φe(s); rule 4: If s ∈ E is an output signal of v ∈ V , then t • (p) = 1 with t = φv(v) and p = φe(s);

A place and its associated cost model respectively a signal and its size. A transition and its ring delay model respectively an operator and its propagation delay. Moreover, a transition with a null delay model each branching point (only b 1 in the example). Its purpose is to allow the placement of registers either before the branching (s 1 ), or on a particular output branch (s 11 , s 12 or s 13 ). The rules 3 and 4 preserve the structure of the net.

All the input signals are considered synchronous, which is equivalent to have them all on the rst pipeline stage. In the model, this corresponds to the initial marking M 0 dened by rule 5: rule 5: If s is an input signal (not outgoing from any operator), then M 0 (p) = 1 with p = φe(s);

The reset action models the placement of a border of pipeline stage, and resets all the clocks of the CRTPN for the following stage. The rule 6 denes the upper bound of the reset interval: rule 6:

I reset = 1 f ;
The time elapsed since the last reset is stored in v(reset). The semantics enforces a reset to happen only if v(reset) ∈ I reset . Then, if the upper bound is xed to 1 f , the pipeline produced has at least a frequency f . Here 1 f , and in the following 1 2f , are supposed to be in N, but they can be rational without altering the results.

The cost function gives the total number of ip-ops needed in the current pipeline stage:

rule 7: We dene P Op = {p ∈ P | ∃t ∈ T Op , t • (p) = 1} and P B (p) = {p ∈ P | ∃t ∈ T B , • t(p) = 1 and t • (p ) = 1}. Then ∀M ∈ {0, 1} P , ω(M ) = p∈P Op C(p) • max(M (p), max p ∈P B (p) (M (p ))).
Indeed, the cost of a place matches with the size of the signal, and consequently with the number of ip-ops needed per register. The cost function manages specically the branching points, where a mutualization of the registers on the output is possible. That explains why the cost of places after a transition modeling a branching point following a place p, is

C(p) • max p ∈P B (p) (M (p )).
These modeling rules are sucient to fully dened the circuit model with CRTPN. All possible pipelines can then be explored thanks to this model. In particular it is possible to nd the optimal one, i.e. the one which minimizes the resource consumed while ensuring a minimal frequency. However, in practice we quickly face a combinatorial explosion during the state space exploration.

To avoid the combinatorial explosion, the two heuristics proposed in [START_REF] Parrot | Pipeline Optimization using a Cost Extension of Timed Petri Nets[END_REF] lead Let q i = (M i , v i ) (0 ≤ i ≤ 14) be the states of this run ρ. The marking of each state after a reset gives the placement of the registers in the pipelined Design and verication of pipelined circuits with TPN circuit. Except for the signals after a branching point: if several are marked, then only one register is needed in the pipelined circuit (mutualization). For example, the marking M 4 = {s 11 , s 12 , s 13 } leads to only one register on s 1 .

The cost of this run is Ω(ρ) = ω(M 0 ) + ω(M 4 ) + ω(M 7 ) + ω(M 14 ) = C(s 0 )+C(s 1 )+(C(s 1 )+C(s 2 ))+(C(s 6 )+C(s 7 )+Cs 8 ) = 61. This cost matches the total number of ip-ops in the pipeline of Figure 8b. On this example, a classical greedy as-soon-as-possible algorithm as implemented in FloPoCo [START_REF] Istoan | Automating the pipeline of arithmetic datapaths[END_REF] (a generator of pipelined arithmetic operators for FPGA), produces the example of Figure 7a, with a total of 94 ip-ops (54% more). The improvement of this approach over the classical greedy has been studied in [START_REF] Parrot | Pipeline Optimization using a Cost Extension of Timed Petri Nets[END_REF], on several arithmetic circuits.

Application to the time-multiplexing

The RTPN model allows exploring many pipelines of a circuit with a frequency guaranteed in an interval. We can check temporal logic properties, such as ensuring that the time spent between the production and consumption of a data on a portion of the circuit is less than a bound. It is in fact possible to impose some specic constraints to the resulting pipelines.

In this section, we apply this approach to the time-multiplexing problem.

As stated in the introduction, we focus here on circuits with a low throughput compared to the clock frequency, thus the whole computation is done in one sampling period.

Folding or time-multiplexing

With an ongoing concern of saving resources, a method called timemultiplexing (also called folding) has been developed. It aims at sharing the instantiation of operators or group of operators which are needed at several places of the circuit. The sharing is secured by sequential access to the instantiation. Figure 9 shows an example of circuit that is suitable for resource sharing (based on an example of [START_REF] Sittel | Model-based hardware design based on compatible sets of isomorphic subgraphs[END_REF]). Suppose that the operators op 1 (resp. op 2 ; op 3 ) and op 1 (resp. op 2 ; op 3 ) are two instances of the same operator. It is then possible to instantiate only once the portions of circuit in (orange) dotted frame, and to share the instantiation. Note that the signal sizes are willingly omitted for ease of understanding, but this approach is still valid with dierent signal sizes (as long as they are equal on the portions to share).

The sequencing of resources access is done with a particular pipeline. Identify this (or one of these) pipeline constitutes the modulo scheduling problem.

A key of the modulo scheduling is to nd the initiation interval : the delay between two introductions of new entries in the circuit. This periodical data introduction can be represented in a RTPN by a token generator on the input. However, as a rst step, we will assume that a new data is introduced once the Fig. 9: Example of time-multiplexing whole computation is done. This assumption is perfectly relevant in signal processing, where the initiation interval (the sampling period) is often signicantly higher than the pipeline period (related to the FPGA frequency).

Our goal is to nd this particular pipeline on the initial circuit containing all the instances, and afterwards to fold the instances (i.e. to merge them).

The pipeline must then verify two properties:

1. The rst is the mutual exclusion. The resources must not be accessible at the same time by several clients.

2. The second concerns the register placement. The registers must be placed on the same locations in the portions of circuit to fold.

In the example Figure 9, the rst constraint means to ensure that there is never some data at the same time on the twin signals: simultaneously in s 5 (resp. It is possible to build this particular pipeline, using the approach presented in Section 4, by guiding the exploration with CTL properties. Thus, the exploration will be restricted to runs verifying those properties. The mutual exclusion can be simply expressed as a marking constraint veried by all states of the run. However, the CTL properties are expressed on markings, they do not allow observing the reset red, which is required by the second constraint.

Design and verication of pipelined circuits with TPN

As the reset is dened in the semantics of the model, it is not explicitly present in the net like the other transitions, it then cannot be connected to an observer place. Somehow the CTL must be extended with the ability to capture the resets red in each place.

Explicit reset

As explained in section 3, due to the density of time the reset can re from an innite number of states with the same marking, but the successor state will always be the same. Therefore, the only relevant ring times are either on the bounds of the interval (I reset and I reset ) or together with a maximal step (in the semantics just after the maximal step ring). One can then consider the reset as a delayable transition with a temporal upper bound, and this preserves the discrete runs. Thus, for all RTPN, a TPN with delayable transitions that veries the same CTL properties can be built.

Indeed, a reset can be explicitly expressed with the pattern drawn in the Figure 10. The place p reset holds a token since the last ring of reset. The delayable transition with delay I reset and the non-delayable transition with delay I reset model the reset interval. For all place p i of the net, the pattern in dashed frame is added and connected to the transitions reset and end_reset. This pattern achieves the reset of the transitions enabled by the place p i . It works in two steps: rst the tokens in the place are drained and temporarily held in p stock i , then once the draining is nished all tokens are set back in the place p i . Each step is based on a zero-test with a loopback which simulates a while loop. In other words, the tokens are removed from p i (resp. p stock i ) while there is some left. Note that with a safe net, the pattern can be greatly simplied: only one zero-test that removes and sets back the token in p i is enough. Denition 11. Let N be an RTPN, and q = (M, v) a state of N . Let the property φ = (reset(p i ) ∼ n) with ∼∈ {<, >, ≤, ≥, =, =} and n ∈ N. The state q veries the property φ if and only if q veries the property ψ = ((M (p obs i ) ∼ n).

Synthesis of a pipeline for the folding

With the RTPN approach and the CTL extension presented previously, it is possible to solve the modulo scheduling problem for the folding of circuits. More specically, it is possible to build a pipeline allowing the folding, while ensuring a minimal frequency and minimizing the number of ip-ops. This solution is applied to the example of circuit given in Section 5.1.

Our method for solving the folding problem is a reachability problem, where a CTL property dene the mutual exclusion. This property allows the state space exploration to be pruned on the y. Thus, the synthesis is guided by the CTL property.

The RTPN model of the circuit of Figure 9 is built using the modeling rules presented in Section 4. It is represented in the Figure 11a. Note that the transitions modeling the shared operators are delayable in order to relax the exploration, and so to satisfy the folding constraints. The places drawn in orange (s 5 , s 6 , s 6a , s 6b , s 8 and s 10 ) are subject to CTL constraints.

A rst atomic property guarantees the mutual exclusion of data in the twin places: φmutex = (M (s5) + M (s8) ≤ 1) ∧ (M (s6) + M (s10) ≤ 1) ∧ (M (s6a) + M (s10) ≤ 1) ∧ (M (s 6b ) + M (s10) ≤ 1). In fact, in the model, tokens represent both the placement of the future registers, and the data propagated when the circuit is pipelined (as soon as pipeline registers are in place). The property φ mutex checks that the two signals s 5 (resp. s 6 , s 6a , s 6b ) and s 8 (resp. s 10 ) will never contain data simultaneously.

A second atomic property guarantees the consistency of registers placement in the twin places in a nal state (state with the nal marking): φconsist = (M (s11) = 1) ∧ (reset(s5) = reset(s8)) ∧ (reset(s6) + reset(s6a) = reset(s10)) ∧ (reset(s6) + reset(s 6b ) = reset(s10)). It checks that in a nal state (M (s11) = 1), the twin places have passed through the same number of reset.

The nal CTL property guarantees that φ mutex holds until it is satised together with φ consist (once a nal state is reached): φ f old = A(φmutexU(φmutex ∧ φconsist)). The pruning during the state space exploration insures that each run saties the property φ f old , as the one presented in Figure 11b. The synthesized pipeline from this run is the one drawn in the Figure 9a.

From the model to the folded circuit

The parts of shareable circuits are currently selected by hand. This problem has been addressed in the literature as automatic identication of isomorphic Design and verication of pipelined circuits with TPN subgraphs, and some solutions have already been proposed [START_REF] Sittel | Model-based hardware design based on compatible sets of isomorphic subgraphs[END_REF]. In our case study, we benet from the high-level abstraction of Matlab/Simulink and some parts of the evaluated models have fairly obvious redundancies to be determined. On the other hand, the use of libraries facilitates the identication of shareable parts.

Once the portions to be shared have been chosen, a minimum bound on the pipeline frequency f p can be deduced from the desired minimum sampling rate f s . Let n be the maximum number of times a circuit portion is shared, then the pipeline frequency must satisfy f p ≥ n • f s . This bound generalizes to the case of sharing nested parts, by multiplying the maximum number of occurrences between nested levels. However, this bound does not guarantee that the resulting folded circuit will have the minimum sampling rate f s . A post-selection of the produced pipelines, based on their latency (which is the sampling period), is therefore necessary. In other words, the lower bound on the pipeline frequency f p is only used to reduce the exploration to a few potential solutions.

Our pipeline synthesis approach for folding has been implemented in a prototype tool. The rst tests are encouraging, and on the example presented, the tool produces the expected pipeline in a few milliseconds: 24ms on an Intel Core i7 xxx processor. The last step is to generate the operators eectively folding the circuit. To do so, the shareable parts are merged, and multiplexers (MUX) are added in the circuit in place of their input/output registers. Figure 12

Conclusion

We proposed a model for the pipeline of synchronous circuit based on TPN à la Ramchandani. Although it allows verication, this model is only able to study one pipeline at a time.

We then focused on the optimization of the pipeline in terms of resources.

The model of RTPN allows generating multiple pipeline with a target frequency, and to select one minimizing the resource consumption with regard to the size of registers and their eventual mutualization.

Using this result we then concentrated on handling together the optimization with the synthesis of pipeline following a specication of temporal logic. In particular, we presented a solution to the time-multiplexing problem. It relies on the explicit expression of the reset in the RTPN model. This method produces a pipeline allowing time-multiplexing, ensuring a target frequency, and minimizing the number of ip-ops.

While these results are encouraging, their implementation may be slow down by the combinatorial explosion. We consider the possibility to combine them with an ILP approach in order to obtain both the computation speed and the possibilities oered by the model-checking. We also think about exploiting further the model-checking towards the interactions with the environment.

Fig. 1 :

 1 Fig. 1: Simulink-to-VHDL compiler dataow diagram.

Fig. 3 :

 3 Fig. 2: Zero-test pattern

Fig. 4 :

 4 Fig. 4: Example of RTPN and some possible runs. Delays are represented in red under the transitions, and delayable transitions are in gray (only t 0 in this example).

Fig. 5 :

 5 Fig. 5: Part of the symbolic state graph of N (until the rst resets)

IFig. 7 :

 7 Fig. 7: An example of pipelined circuit and its corresponding model

7 s 8

 78 A run of the CRTPN of Figure7b. The states following a reset are framed in cyan (q0, q4, q7 and q14) (15:0) (b) A possible pipeline of the circuit of Figure7a

Fig. 8 :

 8 Fig. 8: Example of pipeline synthesized from a run

s 6 )

 6 and in s 8 (resp. s 10 ). The second constraint means that there must be the same amount of registers in the pair of twin signals. That is why the pipeline of the Figure 9b doesn't allow time-multiplexing, contrary to the one of the Figure 9a. Indeed, s 5 crosses no register whereas s 8 crosses one, which violates the second constraint.

Fig. 10 :

 10 Fig. 10: Pattern expressing the reset

Fig. 11 :

 11 Fig. 11: Time-multiplexing with RTPN

Fig. 12 :

 12 Fig.12: Circuit dened in Figure9a folded

  Design and verication of pipelined circuits with TPN From a state (M, v), a transition is reable if it is enabled and its clock is greater or equal to its delay. As for the TPN, the clock of an asap transition t ∈ T D cannot exceed δ(t). Consequently, v(t) ≤ δ(t) and t must re when its clock is equal to its delay. A delayable transition t ∈ T D , may re either when v(t) = δ(t) (not delayed in that case), or when v(t) > δ(t), but in this case t must be associated with at least one (or more) other reable transition t such that v(t ) = δ(t ).

•

, δ, M 0 ) is a TPN; T D ⊆ T is the set of delayable transitions; I reset is the reset time interval with lower (I reset ) and upper (I reset ) bounds in N.

This explains why in the Figure7b, the transitions modeling the operators op0 and op5 are not delayable.

* This work is supported by the Renault-Centrale Nantes chair dedicated to the propulsion performance of electric vehicles.

to good pratical results by limiting the number of delayable transitions 1 and increasing the lower bound of the reset interval.

Pipeline synthesis from the model

Each reachable state of the model represents a pipeline stage that is possible on the real circuit. The reset operation sets the transition from a stage to the following one. The full pipeline is recovered by walking through a branch of the state graph, and accumulating the states following a reset.

Declarations

The authors declare that they have no conict of interest.