DEEQ: Data-driven End-to-End EQuivalence Checking of High-level Synthesis
• During equivalence checking, a data-driven approach is taken to find the correspon- dence of traces between two behaviours. This idea reduces the quadratic search of equivalence traces between two behaviours into a linear one.
A satisfiability problem is formulated to prove or disprove the equivalence of corresponding traces of both behaviours. Our equivalence checker is tool-independent since it does not need any intermediate information from the HLS tool. Experimental evaluations show that our proposed tool is capable of showing the correctness of a commercial HLS tool [10]. Our proposed framework also successfully detected a known bug [72] in Vivado HLS.
The remainder of the chapter is organized as follows. Section4.2presents our equivalence checking Formulation. Equivalence checking between C and RTL-C is presented in Section 4.3. The correctness of the method is presented in Section 4.4. Experimental results and analysis are presented in Section 4.5. Section 4.6 concludes the chapter.
Equivalence Problem Formulation
• h:Qˆ2S ÑU is the update function of the output and the storage variables, where S and U are defined as follows.
´S “ tLYEu is the set of status expressions where L is the set of Boolean literals of the form b or ␣ b, b P B Ď V is a Boolean variable and E is the set of arithmetic predicates over I Y pV ´Bq. Any arithmetic predicate is of the form eR0, where e is an arithmetic expression andR P t““,‰,ě,ą,ă,ďu.
´U is a set of storage or output assignments of the form tx ð e|x P O YV and e is an arithmetic predicate or expression overIY pV ´Bq; it represents a set of storage or output assignments.
q00
q01
q02
q03
q04
q05
q06
- / a ⇐ b + c
- / d ⇐ a - e
¬x < y / x ⇐ x - d x < y /
x ⇐ x + y
- / t ⇐ x + f
- / m ⇐ t - d
- / h ⇐ r + m - / -
a = b + c;
d = a – e;
If (x < y) { x = x + y;
} else { x = x - d;
} t = x + f;
m = t – d;
h = r + m;
(a) (b)
Figure 4.1: Example to illustrate FSMD Model
The FSMD models can be constructed from the high-level representations of the input
DEEQ: Data-driven End-to-End EQuivalence Checking of High-level Synthesis
C code. Any sequential behaviour consists of a combination of three basic constructs: (i) sequences of statements (Basic Blocks) without any bifurcation of control flow, (ii) if-else constructs (Control Blocks), and (iii) loops. Therefore, capturing these three constructs in an FSMD model enables us to effectively represent any sequential behaviour as an FSMD.
The input behaviour basic block consisting of a sequence of n statements s1, . . . , sn, can be represented as a sequence of n + 1 states qi,0, . . . , qi,n, say and n edges of the form qi,j´1 Ý´{sÝÝÑj qi,j, 1ď j ď n, in the corresponding FSMD. However, to reduce the number of states in the FSMD, we first construct a dependence graph for the basic block (BB). The graph consists of a node corresponding to each statement of the BB. There is a directed edge in the dependence graph from the statement s1 to the statement s2 iff there is one of read-after-write, write-after-read, and write-after-write dependencies between s1 and s2. A Control Blocks (CB) is of the form: if(c) then BB1 else BB2 endif, where c is a conditional statement and BB1 and BB2 are two basic blocks that execute when c is true and false, respectively. The FSMD of the CB is obtained from these two FSMDs by (i) merging the start states of two FSMDs into one start state and the end states of two FSMDs into one end state and (ii) the condition c is placed as the condition of the first transition of the FSMD corresponding to BB1 and the condition ␣c is placed in the first transition of the FSMD corresponding to BB2. The FSMD(s) for other control blocks can be constructed in a similar manner. The RTL-C is already a cycle accurate model. The FSMD will follow the control structure of the RTL-C. In fact, FastSim constructs the FSMD first from the datapath and the controller FSM and then represents the same in C. We will use the FSMD constructed by FastSim.
Example 10. Consider the C code and its corresponding FSMD shown in Fig. 4.1 (a) and Fig. 4.1 (b), respectively. The FSMD model the behavioural specification of the model is as follows: M is formally defined as a 7-tuple xQ, q0, I, O, V, f, hy, where
• M = xQ, q0, I, O, V, f, hy, where
• Q = {q00, q01, q02, q03, q04, q05, q06},
• q0 = q00,
• I = tb, c, e, x, y, f, ru,
• O = thu,
Equivalence Problem Formulation
• V = ta, d, t, mu,
• U = taðb`c, dða´e, xðx´d, xðx`d, tðx`f, mðt´d, hðr`mu
• S = txăy,␣xăyu,
• Some typical values of f are as follows: fpq00,ttrueuq “ q01, fpq02,tx ă yuq “ q03, fpq02,t␣xăyuq “ q03,
• Some typical values of h are as follows: hpq02,tx ăyuq “ txðx`yu, hpq02,t␣xă yuq “ txðx´du, hpq05,ttrueuq “ thðr`mu,
l Definition 2. A trace τ of an FSMD is a finite walk from the reset state q0 back to itself and q0 does not occur in between.
A (finite) pathpof an FSMD is a finite walk fromqi toqj, whereqi, qj PQ, is a sequence of state transitions of the formxqi ÝÑci qi`1 ÝÝÑci`1 . . .ÝcÝÝn`1Ñqn “qjysuch that @l, iďlďn´1, Dcl P 2S such that f(ql, clq “ ql`1, and all the states are different, except the end state qj that may be the same as the start state qi. Therefore, a trace is a concatenation of paths.
Definition 3. The condition of execution cτ of a trace τ is a logical expression over I and constants, which must be satisfied by the initial data state inq0 to traverse τ.
Definition 4. The data transformation sτ of a trace τ over O is an ordered tuple xejy of algebraic expressions usingI and constants such that the expression ej represents the value of the output oj after execution of the trace in terms of input variables.
The condition of execution and data transformation of the path can also be defined in a similar manner. The cτ and sτ of a traceτ can be obtained by forward substitution [81].
Example 11. Let us consider the FSMD in Fig. 4.1 (b). It may be noticed that the FSMD consists of two traces: τ0 “ q00 Ñ q01 Ñ q02 ÝÝÑxăy q03 Ñ q04 Ñ q05 Ñ q06 Ñ q00 with cτ0 “ x ă y, and τ1 “ q00 Ñ q01 Ñ q02 ÝÝÝÝÑ␣pxăyq q03 Ñ q04 Ñ q05 Ñ q06 Ñ q00 with cτ0 “ ␣pxăyq. The output expression of traces τ0, and τ1 are r + (x + y + f -b - c + e),
and r + (x + f - 2b -2c + 2e), respectively. l
DEEQ: Data-driven End-to-End EQuivalence Checking of High-level Synthesis
4.2.2 Equivalence of FSMDs
Let the input C behaviour be represented by the FSMD M0 “ xQ0, q0,0, I, V0, O, f0, h0y and the RTL-C be represented by the FSMD M1 “ xQ1, q1,0, I, V1, O, f1, h1y. It may be noted that the inputs and outputs of both behaviours are identical. The V0 of M0 consists of the variables in the input C program. The V1 of M1 consists of registers of the RTL behaviour.
The state transition function may differ since the control structure may be altered due to the application of compiler transformations or by the scheduler. Our main goal is to verify whether M0 behaves exactly as M1. This means that for all possible inputs, the execution traces of M0 and M1 produce the same outputs. So, a trace, which represents one possible execution of an FSMD, takes one assignment of inputs and produces the corresponding outputs. The equivalence of traces and FSMDs are defined as follows.
Definition 5 (Equivalence of traces). A trace τ0 of an FSMD M0 is equivalent to a trace τ1 of another FSMD M1, denoted as τ0 » τ1, if cτ0 ” cτ1 and sτ0 ” sτ1, where cτ0 and cτ1 represent the conditions of execution ofτ0 and τ1, respectively andsτ0 and sτ1 represent the data transformations of τ0 and τ1, respectively.
Definition 6 (Containment of FSMDs). An FSMDM0 is said to be contained in an FSMD M1, symbolically M0 ĎM1, if @τ0 PM0,Dτ1 PM1 s.t. τ0 »τ1.
Definition 7 (Equivalence of FSMDs). Two FSMDs M0 and M1 are said to be computa- tionally equivalent, i.e., M0 »M1, if M0 ĎM1 and M1 ĎM0.
For deterministic model, one way containment implies equivalent, i.e., M0 Ď M1 ùñ M0 »M1 since the union of conditions of execution of all traces in M0{M1 is True [46].