Information Technology Reference
In-Depth Information
L 0;
T #ByteValue;
A #Bit0;
JC BIT1;
L 1;
T #ByteValue;
BIT1: AN #Bit1;
JC BIT2;
L #ByteValue;
L 2;
+I;
T #ByteValue;
<ACCU2> = <ACCU1>;
<ACCU1> = 0;
#ByteValue = <ACCU1>;
(1)
#ByteValue = 0;
(1)
(2)
#Bit0 == 1 ?
(2)
no
yes
(3)
#ByteValue = 1;
(3)
if (</FC>)
<RLO> = (#Bit0 | <OR>) & <RLO>;
else
<RLO> = (#Bit0 | <OR>);
fi
</FC> = 1;
if (<RLO>)
</FC> = 0;
<OR> = 0;
<STA> = 1;
goto BIT1;
fi
(4)
(4)
#Bit1 == 0 ?
no
yes
(5)
#ByteValue += 2;
(5)
BIT2: ...
Control Data Flow Graph
Hardware Realization
Source Code (IL)
Fig. 1. Faulty program
from the same component, simultaneously. The CDFG is extended by cor-
rection logic, the input stimuli (
I
) is constrained to the values of the failure
trace, and the observation points are restricted to the expected responses
(
v
expected
(
).
The initial debugging instance is contradictory, due to the constrained ex-
pected responses at the observation points
OP
i
. Correction-based debugging
resolves the conflict by activating exactly
k
abnormal predicates. Thereby,
k
gives the cardinality of the fault candidate and may be a single fault (
k
OP
i
)
=1
)
or a multiple fault (
k>
,
k
is incremented as long
as the instance is still contradictory. A
cardinality constraint
controls the
activation of abnormal predicates. The debugging model is translated into
Conjunctive Normal Form
(CNF) and given to a
Boolean satisfiability solver
(SAT solver) to declare the instance satisfiable or unsatisfiable. After the
conflict is resolved, i.e. the instance is satisfiable, fault candidates of minimal
cardinality are obtained.
1
). Starting with
k
=1
4
Evaluation
The debugging methods are evaluated on concrete benchmarks in the follow-
ing sections. A detailed case study is presented in Section 4.1 to highlight
the pro and cons of the debugging techniques. Experimental results for the
application on industrial benchmarks are given in Section 4.2.
4.1
Case Study
An example is used to illustrate the approaches. Figure 1 (left) shows a part
of a combinational IL program. The program converts the eight inputs (
Bit
0
