Background Review
2.3 PN: Petri Net
Petri Net is a graphical and mathematical modeling tool applicable to many applications, especially the parallel or concurrency systems. The primary concept was original from Carl Adam Petri in his Ph.D thesis since 1962 [65]. Readers may refer more literatures about history and survey works from [66–73].
Formally, a Petri Net GP N(P, T, W, M0) can be represented by a four-tuple graph [70], where P = {p1, . . . , pn} and T = {t1, . . . , tm} are finite sets of place and transition, W is the weighted flow relation, and M0 is the initial marking.
Visually in graph, places are drown as circles and transitions as boxes or bars.
A marking (state) is a mapping function M : P → {0, 1, 2, · · · }. If M (pi) = k for place pi, we say that place pi is marked with k tokens. In graphic, we draw k block dots (tokens) inside place pi if M(pi) = k. The initial marking M0 denotes the number of tokens that all places are marked initially. A marking M is said to be a valid state if and only if M (pi) > 0, ∀pi ∈ P . Let u and
v be two arbitrary adjacent nodes of PN. If W (u, v) > 0, then there is an arc from u to v with weight W (u, v). In this research, we assume that W (u, v) = 1 for each node pair. For a node u in P ∪ T , •u (the pre-set of u) is specified by: •u = {v ∈ P ∪ T |W (v, u) > 0} and u• (the post-set of u) is specified by:
u• = {v ∈ P ∪ T |W (u, v) > 0}. In our work, for each place pi ∈ P , we only alow pi has only one output transition, that is ∀pi ∈ P, |pi•| = 1.
When considering a condition-event system, places with marking (state) rep-resent the conditions, while transitions reprep-resent the events. A transition (event) has certain number of input and output places representing the pre-conditions and post-conditions of the event. The presence of a token in a place is interpreted as holding the truth of the condition associated with the place. In [67], the author gave some typical interpretations of places and transitions. We redescribe these interpretations in Table. 2.2.
Table 2.2: Typical interpretations of places and transitions Input places Transition Output places
Preconditions Event Postconditions
Input data Computation step Output data Input signals Signal processor Output signals Resources needed Task or job Resources released Conditions Clause in logic Conclusions
Buffers Processor Buffers
The execution of a Petri Net is controlled by the number and distribution of tokens. Tokens reside in the places and control the execution of the transitions of the net. A Petri Net executes by firing transitions. A transition fires by removing tokens from its input places and creating new tokens which are distributed to its output places. A transition may fire if it is enabled. A transition tr is enabled at marking M (denoted by M[tri) if ∀p ∈•tr : M (p) > W (p, tr). Once a transition tr is enabled at M, it may fire and then reach a new marking M′ (denoted by
M[tri M′). The occurrence of tr lead to a new marking M′, defined for each place p by
M′(p) = M (p) − W (p, tr) + W (tr, p) . (2.5)
A sequence of transitions σ = tr1· · · trk−1 ∈ T∗ is a firing sequence from a marking M1 to a marking Mk if and only if there exist markings M2, . . . , Mk−1
such that
Mi[trii Mi+1, for 1 6 i 6 k − 1. (2.6)
Marking Mk is said to be reachable from M0 if and only if there exists a firing sequence σ : M0[σi Mk. [Mi is the set of markings reachable from M by firing any sequence of transitions, i.e., M′ ∈ [Mi ⇔ ∃σ ∈ T∗ : M[σi M′. [M0i is the set of all markings reachable from M0.
Matrix representation of PN is defined by incidence matrix A (also called the characteristic matrix), which is a |P | × |T |-matrix with entries
Aij = W (trj, pi) − W (pi, trj) . (2.7)
The matrix representation usually gives a complete characterization of PN.
Let xj = {trj} = (. . . , 0, 1, 0, . . .) be the unit |T | × 1 column vector which is zero everywhere except in the j-th element. Also, let µ is the |P | × 1 column vector respected to a marking M0 with entries µi = M0(pi). The transition trj
is represented by the column vector xj. A transition trj is enabled at a marking M0(denoted by M0[trji) if µ > A · xj. And the result marking, µ′, of firing enabled transition trj in a marking µ0 is represented by
µ′ = δ (µ0, trj) = µ0+ A · xj. (2.8)
Where δ : M × T → M is a transition function mapping current marking state µ0 and current firing transition into the next next marking state µ′. For a sequence of transition firing σ : M0[σi Mk and Mi[trii Mi+1, 1 6 i 6 k − 1, we have:
δ (µ0; σ) = δ (µ0; tr1tr2tr3. . . trk−1)
= µ0+Pk−1 1 A · xj
= µ0+ A · f (σ) .
(2.9)
The vector f (σ) is firing vector of the sequence σ = tr1. . . trk−1. The i-th element of f (σ), f (σ)i∈ Z, is the number of times that transition tri fires.
The reachability tree is the important technique analyzing the reachability marking set of a PN model. The tree structure shows which states of the PN can be reached with arbitrary transition firing sequences starting from the initial marking state M0. A reachability tree is a hierarchical graph with directed arcs.
The nodes of the tree represent PN marking state and the arcs represent transi-tions firing. The root node represents the initial net state and the leaf nodes are reachable net states. Duplicate nodes reflect multiple net states in the tree. The terminal nodes represent the end of valid paths through the tree and can also rep-resent net states. To prevent infinite number of markings which result from loops in a PN model, a special symbol ω is introduced in reachability analysis [66, 67].
For any constant a, ω is defined by:
w + a = w w − a = w a < w w 6 w
(2.10)
By using ω notation, an PN tree constructing algorithm is given in Algo-rithm. 3. An example PN is given in Figure. 2.8(a), and its reachability using ω notation is given in Figure. 2.8(b).
Algorithm 3 Algorithm of constructing a reachability tree from a PN
1: Initialize the root node of the tree with x = µ0
2: for all node µ to be inserted, evaluate δ(x, trj), ∀trj ∈ T do
3: if δ(x, trj) is undefined, ∀tj ∈ T then
4: the x is a terminal node
5: else if δ(x, trj) is defined for at least one trj ∈ T then
6: create a new node x′ = δ(x, tj)
7: if x′(pi) = ω, ∀pi ∈ P then
8: defien x′(pi) ← ω
9: else if a node y exists and x′(pi) > y(pi), ∀pi∈ P then
10: set x′(pi) ← ω, ∀pi ∈ P
11: else
12: x′(pi) ← x′(pi)
13: end if
14: end if
15: end for
16: if all nodes are either terminal nodes or duplicate nodes then
17: stop tree construction
18: end if
p1
p2
p3 t1 p4
t2
t3
1 0 1 0
1 0 0 1
1 w 1 0
1 w 0 0
1 w 0 1
1 w 1 0
t3 t2
t1
t3 t2
(a) (b)
Figure 2.8: (a) A Petri Net to illustrate the construction of a reachability tree, (b) the reachability tree of the Petri Net
CHAPTER 3
Modeling and Formal Verification of Dataflow Graph in System-Level Design Using Petri Net
3.1 Introduction
In this chapter, we address a PN (Petri Net) based formal verification method for dataflow or DSP-driven algorithms of HLS (High-Level Synthesis) result. Tradi-tionally, given a DSP-driven algorithm, the arithmetic transformations [60], such as retiming and unfolding techniques [59, 61], and the scheduling techniques are used to achieve optimal system specification goals in HLS. These system-level design techniques are usually applied iteratively and error-prone. In order to detect design faults of system-level design, system-level verification is introduced in design flow. In this work, two-phases verification including static and dynamic phases are proposed, and Figure. 3.1 illustrates the verification flowchart.
As showing in flowchart, the dataflow algorithm is usually represented by a Fully-Specified Signal Flow Graph (FSFG). To check a DSP-driven algorithm in PN domain, the design is first converted into a PN (Petri Net) model by using proposed conversion method and then apply verification techniques in PN domain. In static phase, the target is to verify the arithmetic transformations of HLS. Since, the procedures of retiming or unfolding in FSFG domain can be seen a serial token movement in PN domain, the verifier can check the correctness of
the arithmetic transformations by checking the validation of PN token movements in PN domain.
In dynamic phase, PN model is used to verify the schedule schemes of given FSFG. In order to map DSP algorithm on a hardware circuit, scheduling tech-niques are applied to find suitable schedules of FSFG. For high performance issues, such as smaller silicon area, higher throughput rate, and lower power consumption, these algorithms start from as-late-as-possible (ALAP) to as-soon-as-possible (ASAP) schedule time and assign the starting time of each task of FSFG [74]. The execution of all tasks is referred to as an iteration. Within an iteration, the execution sequences are different from various scheduling al-gorithms, but the original behavior is not changed. Once a schedule scheme of FSFG is produced from scheduling algorithms, the permanent behavior of system and schedule scheme are transformed and verified in PN domain as well in static phase.
The PN-based verification can be considered as a model checker with ca-pability of checking a number of properties that should be hold under system specification. In PN domain, the inputs to the model checker include a char-acteristic matrix describing the system and the system properties described in matrix equations. By applying mathematics theory and matrix manipulation, the model checker reports whether the design is valid. When comparing with FSFG, designing DSP algorithm at FSFG domain and verifying it at PN do-main provides double-checking verification solution. Additionally, PN theory also provides primary property analysis techniques of system, such as reachabil-ity, liveness, safeness, boundedness, and reversibility [75] that FSFG can not be offered.
This chapter is organized as follows. First, we describe the methodology of
Algorithm Development
Algorithm
transformation System
static model using Petri net Static
Verification
Algorithm scheduling assignment
Dynamic Verification
System dynamic model
using Petri net System level design
(In FSFG domain) Petri Net Based Verification Design
specification
Resources Goals and constraints
High level optimization
Scheduling and Resource Allocation
RTL Level
Figure 3.1: System-level design flow and the PN-based verification
conversion from FSFG to PN model. Then, PN based high-level verification flow is presented in Section. 3.3. In Section. 3.4, we introduce our verification software application tool called HiVED (High-Level Verification Engine for DSP) and show some experimental results. Finally, we make some concluding remarks in the latest section.