Background Review
3.3 High-Level Verification
In last section, we have addressed the conversion method to convert a FSFG graph into PN domain and use PN characteristic matrix to represent a design system. Since, retiming process or tasks executing for the HLS of the original FSFG design can be seen token movement of PN model in PN domain. Therefore, we can use PN theory to check the correctness of arithmetic transformations or scheduling of HLS. In the following, two-phases verification method including static and dynamic phases are presented.
3.3.1 Static Verification
The target of the static phase verification is to verify the arithmetic transfor-mations including the unfolding and retiming techniques. In FSFG domain, the arithmetic transformations are applied to the original FSFG design attempting to obtain optimal FSFG [59–61]. These optimization techniques are typically used to reduce the critical path delay, silicon area, number of latches and power consumption. However, these algorithms are error-prone and have a lot cost that limits their use. High-level verification for the arithmetic transformations can check the correctness of HLS in the early stage of the design flow. In design-ers’ point of view, if we can quickly tell whether the HLS result of the design is correct, then the redesigning time or costs can be reduced.
The flowchart to the static phase verification flow is shown in Figure. 3.7. In HLS, designs may apply arithmetic transformations on DUV design iteratively in their design flow. We have stated in previous section that the designing pro-cedures of arithmetic transformations can be seen a serious token movements in PN domain. The designing parameters, which include delay Ri, unfolding factor
f , and final delay Rf of DUV, are transformed into PN model as initial token µ0(|P |×1), unfolding factor f , and final token µ′(|P |×1) with respect. While com-paring to the unfolding technique in FSFG domain, the converted PN model is also unfolded in PN domain. Before applying retiming checking, we first address unfolding algorithm of PN model in next section.
(
0)
: '
x µ n µ A x
∃ − ⋅ = ⋅
Original FSFG design
Retimed FSFG
Unfolded PN Model Retiming
algorithm
Unfolding algorithm
Unfolded FSFG Arithmetic transformations
Rf, f Ri
Unfolding algorithm
Set of properties:
A, Di, Df
true false FSFG domain Petri net domain
DUV
Figure 3.7: Flowchart of static phase verification.
3.3.2 PN Unfolding
Let A(|P |×|T |) and d(|P |×1) be the characteristic matrix and the initial delay vector of a PN model. Assuming its unfolding PN model has PN matrix A′f ·|P |×f ·|T |
and initial delay vector bd(f ·|P |×1). For each element a′(i, j) in A, there is a sub-matrix bi,j in dimension (f × f ) with it. The value of all element bi,j(s, t) and bdi(s) depend on delay d(i) and following PN unfolding Algorithm. 4.
Algorithm 4 Unfolding a Petri Net by f
1: for all s = 1, 2, · · · , f and t = 1, 2, · · · , f do
2: if d(i) = 0 then
3: bi,j(s, s) = 1
4: bdi(s) = 0, s = {1, 2, · · · , f }
5: else if d(i) < f then
6: if a(i, j) = 1 then
7: bi,j(s, s) = 1
8: else if a(i, j) = −1 then
9: bi,j(s, s + d(i)) = −1, s = {1, 2, · · · , f − d(i)}
10: bdi(p − s + 1) = 1, s = {1, 2, · · · , d(i)}
11: end if
12: else if d(i) = f then
13: if a(i, j) = −1 then
14: bij(s, s) = −1
15: else if a(i, j) = 1 then
16: bij(s, s) = 1
17: bdi(s) = 1, s = {1, 2, · · · , f }
18: end if
19: else if d(i) > f then
20: if a(i, j) = −1 then
21: bi,j(s, s) = −1
22: else if a(i, j) = 1 then
23: bi,j(s, f − mod(d(i), f ) + 1) = 1,
24: bdi(s) = ⌈d(i)/p⌉, s = {1, 2, · · · , mod(d(i), f )};
25: bi,j(s + mod(d(i), f ), s) = 1,
26: bdi(s) = ⌊d(i)/f ⌋, s = {1, 2, · · · , f − mod(d(i), f )}.
27: end if
28: end if
29: end for
Di=[1 0 0 1]-1
Figure 3.8: (a) A example PN model, (b) the 2-folded PN model , (c) PN char-acteristic matrix of (a) and (d) PN charchar-acteristic matrix of (b)
Figure. 3.8(a) is an example PN model, and Figure. 3.8(b) is its unfolded PN model by using the above rules. Figure. 3.8(c) and (d) are the PN characteristic matrices of (a) and (b) respectively.
3.3.3 Retiming
After applying PN unfolding rule, the unfolded PN model with PN characteristic matrix, initial and final marking states are used to check the correctness of retim-ing process. Let µ0 be the initial marking state, A be the characteristic matrix, x be the firing transition vector and µ′ be the marking state after x firing. The firing process can be expressed by a matrix equation by Equation. (2.8) and is rewritten by Equation. (3.1):
µ′ = µ0+ A · xj. (3.1)
The delays of FSFG can also be scaled by a positive integer number n without affecting the functional behavior of the FSFG, thus it becomes:
µ′ = n · µ0 + A · x, or A · x = (µ′− n · µ0) . (3.2)
By using linear system theory [76], equation y = A · x has a unique solution x if and only if matrix [A] and matrix [A|y] have the same rank. In our case, y = (µ′− n · µ0) is known and A is the characteristic matrix of PN. Therefore, we can check the correctness of HLS result by checking the equivalence of the matrix rank. Finally, as showing in Figure. 3.7, the verifier reports true if x has solution and false else.
3.3.4 Dynamic Verification
In dynamic phase, the target is to verify the tasks executing schedule of FSFG design. The flowchart to the dynamic verification flow is shown in Figure. 3.9.
In FSFG domain, scheduling algorithms are applied to the FSFG and produce desired schedule schemes. A schedule of a given FSFG includes the start time s(j) = tj and execution delay c(j) = dj of each PE (process element) vj of FSFG, that is:
s(vj) = {tj ∈ N|0 ≤ tj ≤ IP }, (3.3)
c(vj) = {dj ∈ N|vj ∈ V = {v1, · · · , vn}}. (3.4)
Within one iteration period (IP), a schedule scheme gives the executing se-quence of all PE of V . Generally, various schedule schemes that need to be verified are either solved by Integer Linear Programming (ILP) [74, 77] or found by heuristic method. The solution of schedule scheme is in binary decision vari-able matrix X or Gantt chart form. When a schedule of FSFG design is produced, the DUV schedule and the original FSFG are transformed into PN model. As describing in previous section, moving tokens between places is meaning firing the executable transitions. Thus, schedule verification in PN domain can be seen as PN reachability problem.
Considering timing interval within one IP, the marking µl, where l ∈ N and 1 ≤ l ≤ IP is the token state of the corresponded time step. For each time step l, the executable PE set xl is defined as:
xl = {vj ∈ V |s(vj) + c(vj) − 1 = l}. (3.5)
Therefore, there exists firing sequence set σ in PN domain with respected to xl in FSFG domain. The verifier check whether there is only one initial marking M0 for each time step that satisfied the following equation:
∃M0 : M0[σiMl. (3.6)
Original FSFG design
Schedule Scheme (DUV) Scheduling
algorithms Petri Net Model
Petri Net domain FSFG domain
Set of properties:
A, s Schedule
true false
M
lM M
0:
0[ σ
∃
Figure 3.9: Flowchart of dynamic phase verification.