machine of manageable size from the cone of influence of the FSM. Once a livelock is found on an abstract machine, the livelock is justified on the concrete machine with trace concretization. Experimental results shows that the proposed abstraction-based livelock checking finds real livelock errors in industrial designs.
Livelock/deadlock is a well known and important problem in both hardware and software systems. In hardware verification, a livelock is a situation where the state of a design changes within only a subset of the states reachable from the initial states of the design. In a state transition graph, a livelock is a set of states from which there is no path going to any other states that are reachable from the initial state. Since deadlock is a special case in which there is only one state in a livelock, deadlock checking can be done by livelock checking. Thus, livelock implies both livelock and deadlock in this paper. However, livelock checking1 has never been actively used in hardware verification in practice, mainly due to the complexity of the computation which involves finding SCCs (Strongly Connected Components). Thus, livelock checking has been on hardware designer’s wish list to verify their designs.
There have been many approaches on finding SCCs [
In this paper, we first present an improved BDD-based
algorithm finding TSCCs from[
This paper also presents a practical approach for checking
livelock using abstraction techniques. The proposed
livelock checking works on FSMs(Finite State Machines)2 rather
than the whole design. For each FSM, we make an abstract
machine (by localization reduction [
Once an FSM is given, its COI is first computed. Then,
an abstract machine is computed by finding N in uential
latches from the COI. Influential latches are the latches that
are likely related with the FSM. N is either pre-defined or a
user-defined number of latches in the abstract machine, or
1Livelock checking is different from liveness checking and
the difference will be explained in Section 2.3.
2FSMs are either automatically extracted [
There is another important hardware property called toggle deadlock. A state variable has a toggle deadlock if the state variable initially toggles and the state variable becomes a constant after a certain number of transitions. However, notice that this is not a constant variable since it initially toggles. Toggle deadlock may or may not happen depending on input stimuli in simulation. Therefore, toggle deadlock is also an important property to check with formal approaches.
Experimental results shows that the proposed abstractionbased approach finds real livelock and toggle deadlock errors from industrial designs.
The contributions of this paper are in the three aspects. • Improved algorithm for livelock checking
The proposed algorithm improved the existing
algorithm [
This paper presents theories and an implementation on abstraction-based livelock checking to handle large designs in practice. • Toggle deadlock checking
To the best of our knowledge, this paper presents the first method to solve toggle deadlock problem.
The remainder of this paper is organized as follows. Section 2 briefly recapitulates finding SCCs and TSCCs, and describes related work. Section 3 describes our improved algorithm for finding TSCCs. Section 4 explains how livelock is checked on FSM using abstraction. Section 5 describes how to check toggle deadlocks. Experimental results are presented and discussed in Section 6. We conclude with Section 7. 2. 2.1
Given a graph, G = (V; E) where G is an infinite transition
system of the Kripke structure [
Finding SCCs has a variety of applications in formal
verification such as Buchi emptiness [
The traditional approach to find SCCs is to use Tarjan’s
method [
To overcome this state explosion problem in explicit
algorithms, there have been many publications on symbolic
algorithms. Ravi et al. [
Even though TSCCs are a subset of SCCs in the states of a design, the algorithms for finding TSCCs can be significantly optimized since not all SCCs are of interest.
This section recapitulates the work on finding TSCCs by
Xie and Beeral [
Definition 1. The forward set of state i ∈ S, denoted by F (i), is the set of states that have a path from i. That is, F (i) = {j ∈ S | i → j}. Similarly, the backward set of state i, denoted by B(i), is the set of states that have a path to i. That is, B(i) = {j ∈ S | j → i}.
Lemma 1. Let i; j ∈ S. If j ∈ F (i), then F (j) ⊆ F (i). Similarly, if j ∈ B(i), then B(j) ⊆ B(i).
Theorem 1. A state i ∈ S is recurrent if and only if F (i) ⊆ B(i). In other words, i is transient if and only if F (i) * B(i).
Theorem 2. If state i ∈ S is transient, then states in B(i) are all transient. If state i is recurrent, on the other hand, states in F (i) are all recurrent. In the latter case, set F (i) is a recurrence class, and set B(i)\F (i) (if not empty) contains only transient states.
Lemma 1, Theorem 1 and 2 are from [
There are two types of properties in model checking; safety
and liveness properties [
Livelock checking is different from liveness checking in the sense that liveness checking requires a liveness property to work on a design, whereas livelock checking does not require any property and works on a design directly.
There have been many publications on finding all SCCs [
Hachtel et al. [
Qadeer et al. [
Xie and Beeral proposed a reachability-based algorithm
to find all TSCCs iteratively [
None of the above previous work on finding TSCCs was used in real designs in practice, due to the design sizes. Our abstraction-based approach is the first in publication to handle large designs in practice.
Case et al. [
The state classification in [
We propose a new state classification that is shown in Figure 1, assuming that there is one single initial state. Handling multiple initial states is explained in Section 3.3.
Definition 2. STSCC is a sink TSCC that has incoming edges from any states outside the TSCC.
We first define sink TSCC (in short, STSCC) in
Definition 2. The new state classification consists of main group,
transient group, livelock groups (reachable STSCCs) and
unreachable TSCCs for a given initial state. The transient
class in [
Reachable States
c a
b Main Group k
l j
Unreachable TSCC m g o n
i d e f h
Livelock Group
Transient Group (Reachable STSCC)
In Figure 1, there are states a through o and a is the initial state that is marked with thick circle. Among all states, the reachable states are a through i inside the dotted rectangle. The unreachable states are j through o outside the dotted rectangle. There are five SCCs that are {a; b; c}; {e; f; g}; {h; i}; {j; k; l}; and{m; n; o}. Since a is the initial state, {a; b; c} becomes the main group. {h; i} and {m; n; o} are TSCCs and only {h; i} is a livelock group (reachable STSCC) since it is reachable from a. {m; n; o} is called an unreachable TSCC. The rest states, {d; e; f; g; j; k; l}, belong to the transient group in which the states are contained in neither the main group nor the TSCCs. 3.2
We first define transition relation in Definition 3 to explain our algorithms to check livelock.
Definition 3. Let x = {x1; : : : ; xn}, y = {y1; : : : ; yn}, and w = {w1; : : : ; wp} be sets of variables ranging over B = {0; 1}. A ( nite state) machine is a pair of boolean functions ⟨Q(x; w; y); I(x)⟩, where Q : B2n+p → B is 1 if and only if there is a transition from the state encoded by x to the state encoded by y under the input encoded by w. I : Bn → B is 1 if the state encoded by x is an initial state. Q(x; w; y) is called transition relation. The sets x, y, and w are called the present state, next state, and input variables, respectively.
The procedure ComputeF orwardSet in Figure 2 is a
modified version of the procedure f orward set in [
ComputeBackwardSet is a dual procedure to Compute F orwardSet, except not using stop and not computing the onion rings O.
Figure 3 is a procedure for finding TSCCs from the given
set of states S. The procedure F indT SCCs is a modified
version of the procedure State classif ication in [
Figure 4 shows the procedure to perform our new state classification. As explained in Section 3.1, we find main group (M ), transient group (T ), and livelock groups (R) from the given initial state (s) within the given care states (S). F indLivelock starts computing forward set F (s) and backward set B(s) in Line 1 and 2. In Line 3, reached is the reached states from s in S. If F (s) ⊆ B(s) in Line 4, there is no livelock in S. In this case, F (s) becomes the main group and both R and T are set to empty in Line 5-7. If F (s) * B(s) in Line 8, there must exist at least one livelock group. In this case, M is computed by intersecting F (s) and B(s) in Line 9. careSet is set to a subset of F (s) in Line 10. The lasso prefix states in careSet are trimmed out in FindTSCCs(Q, S) {
R = { }; T = ZERO; careSet = S; while (careSet ̸= ZERO) { s = PickOneState(careSet); B(s) = ComputeBackwardSet(Q, careSet, s); F (s) = ComputeForwardSet(Q, careSet, s, ¬B(s)); if (F (s) ⊆ B(s)) {
R = R ∪ F (s); T = T ∨ (B(s) ∧ ¬F (s)); careSet = careSet ∧ ¬B(s);
TrimTransient(Q, careSet, T , PREFIX); } else {
T = T ∨ (s ∨ B(s)); careSet = careSet ∧ ¬(s ∨ B(s));
TrimTransient(Q, careSet, T , BOTH);
}
}
return (R; T );
is not necessarily all state space. T is a set of transient states
in S, and R is an array of TSCCs in S. P ickOneState in
Line 5 picks a random state from careSet as a seed state to
find a TSCC. In Line 7, early termination is used in
computing the forward set F (s), by setting stop in Figure 2 as the
negation of B(s). This is because while we compute F (s)
within B(s) for the state s, once any state outside B(s)
is reachable from s, all states in B(s) are transient.
Another big difference is trimming transient states in Line 12
and 16. T rimT ransient(Q; careSet; T; dir) trims out the
transient states from the current care states by the given
direction (dir) that is either PREFIX, SUFFIX, or BOTH.
PREFIX(SUFFIX) means to trim out the lasso prefix(suffix)
states. This is the same technique used in finding SCCs [
Line 11. TR represents the set of transient states that are reachable from s. In Line 12, R and TR are computed by calling F indT SCCs with careSet. If s ∈= M (means that the main group is empty), s is added to TR in Line 13-14. TU represents the set of transient states that are unreachable from s and TU is computed in Line 15. T is computed by union of TR and TU in Line 16. 3.3
It is possible for a design to have multiple initial states when some of the state variables do not have concrete initial values. In the presence of multiple initial states, finding livelock groups has to be devised correctly to avoid false positives and redundant computations.
Figure 5 shows an example with multiple initial states. In this example, there are six states, S = {a; b; c; d; e; f }. There are two SCCs, {a; b; c} and {d; e; f }. We can see that {d; e; f } is a TSCC. a and d are initial states, I = {a; d}, as shown with thick circles. Suppose that we compute livelock by calling F indLivelock(Q; S; I). Then, we get F (I) = B(I) = M = {a; b; c; d; e; f } and R = {} which is not correct since there is a reachable TSCC. Now, let us try to call F indLivelock for each single initial state. First for the initial state a, we get F (a) = {a; b; c; d; e; f } and B(a) = {a; b; c}. This gives us Ma = {a; b; c} and Ra = {d; e; f }. There is a livelock group Ra for the initial state a. Now, for the initial state d, F (d) = {d; e; f } and B(d) = {a; b; c; d; e; f }. This gives us Md = {d; e; f } and Rd = {} and TU = {a; b; c}. There is no livelock group for the initial state d. Therefore, we can see that livelock checking has to be applied for each single initial state separately in the presence of multiple initial states.
c
f a b d
e
Theorem 3. When there are two initial states (i0 and i1), if i1 is included in the reached states from i0, the livelock groups from i1 are a subset of the livelock groups from i0.
Proof. Since i1 is included in the reached states from i0, i1 is in either main, transient, or livelock groups from i0. When i1 is in the main group, the same livelock groups from i1 are obtained. When i1 is in the transient group, all or a subset of the livelock groups i1 is obtained. When i1 is in one of the livelock groups, the livelock group including i1 becomes the main group from i1, and no livelock group exists from i1 since the other livelock groups from i0 become unreachable TSCCs from i1. From the above three cases, no new livelock group is obtained from i1 compared to the ones from i0. Therefore, the livelock groups from i1 are a subset of the livelock groups from i0.
Theorem 3 says that when there is large number of initial states, we can skip livelock checking for any initial states that are already in the forward sets of other initial states. In Figure 5, livelock checking for the initial state d can be skipped because of d ∈ F (a), assuming that a is used first. However, there is an order dependency on which initial state is used first. If d is used first, we still need to run livelock checking with a. In practice, the number of calls to F indLivelock is greatly reduced because of Theorem 3 in the presence of multiple initial states.
Figure 6 is the top-level procedure that checks livelock with multiple initial states. CheckLivelock takes transition relation(Q), a set of states(S), a set of initial states(I), and a concrete machine(C) as procedure inputs. The use of C is explained in Section 4. CheckLivelock first finds livelock groups in the reachable states in Line 1-17 and then it finds TSCCs in the unreachable states in Line 18-23. The while loop (Line 6-17) performs livelock checking for a current initial state s until all initial states are covered with iteration index k. For this, remaining is initially set to I in Line 3 and updated by eliminating the newly reached states reachedk from remaining in Line 13. reached is the reached states from all initial states. reached is initially set to ZERO in Line 1 and updated by adding reachedk that is the reached states from s in Line 12. Then, the next initial state is chosen from remaining in Line 15. TU is the union of unreachable transient states from each initial state. TU is initially set to ZERO in Line 2 and updated by adding the unreachable states of Tk in Line 14. For the current initial state s, F indLivelock is called in Line 7. |Rk| represents the number of livelock groups in Rk in Line 8. For each Rkj, a trace tracejk is generated in Line 9 and the livelock is reported with the trace in Line 10. Generating trace is explained in Section 4.2 and reporting livelock is explained in Section 4.3.
CheckLivelock(Q, S, I, C) { reached = ZERO; TU = ZERO; remaining = I; k = 0; s = PickOneState(I); while (s ̸= ZERO) { (Mk; Rk; Tk; reachedk; Ok) = FindLivelock(Q, S, s); for (j = 0; j < |Rk|; j++) { tracejk = GenerateTrace(C, Rkj, s, Ok); ReportLivelock(s, Mk, Rk, Tk, tracejk);
j } reached = reached ∨ reachedk; remaining = remaining ∧ ¬reachedk; TU = TU ∨ (Tk ∧ ¬reachedk); s = PickOneState(remaining); k++; } careSet = ¬(reached ∨ TU ); if (careSet ̸= ZERO) {
Rk = FindTSCCs(Q, careSet); for (j = 0; j < |Rk|; j++)
ReportUnreachLivelock(Rkj);
To check whether a livelock exists in a design or not, the checking should be done on the whole design. However, this is infeasible due to the size of the design in practice. Thus, we propose a practical method for checking livelock on FSMs on the design.
Even when we check livelock on an FSM, the entire COI logic of the FSM must be considered in order to get an exact result on livelock. However, this is still computationally very expensive or not feasible, in most real designs. Thus, we propose a framework for abstraction-based livelock checking on an abstracted COI of the FSM. Once we find a livelock on the abstract machine, we justify whether the livelock exists on the concrete machine. Notice that a livelock on the abstract machine can be mapped into more than one livelock on the concrete machine.
Figure 7 shows how an abstract machine is obtained from the COI of an FSM. Suppose an FSM that has two state variables f and g. Then, we compute the COI of the FSM. Suppose that there are state variables {a; b; c; d; e} in the COI of the FSM. The size of the abstract machine is predefined and let us suppose that the size is N . Then, a set of influential latches from the COI is computed from the FSM variables. The minimum abstract machine is the FSM itself and the maximum abstract machine is the concrete machine. In this example, N =4 and we get the abstract machine {f; g; d; e}.
COI of FSM a b c d e
FSM f g
Concrete Machine
Theorem 4. If any state in a livelock group on an abstract machine is reachable from the initial state on the concrete machine, the livelock exists on the concrete machine.
Proof. Since the abstraction is an over-approximation, the set of all transitions on the abstract machine is a superset of the set of all transitions on the concrete machine. Since there is no path from any state in the livelock group to any state in the main group on the abstract machine, there is still no path from any projected states of the livelock group on the concrete machine to any projected states of the main group on the concrete machine. Now, suppose that the livelock does not exist on the concrete machine. In order for the livelock not to exist on the concrete machine, the only condition is that there is no path from the projected main group to the projected livelock group on the concrete machine. In other words, the projected livelock group has to be unreachable from the initial state. However, this contradicts the assumption that any state of the livelock group is reachable from the initial state on the concrete machine. Therefore, the livelock group still exists on the concrete machine.
Thanks to Theorem 4, this abstraction-based livelock finds a livelock on small abstract machine using BDD-based symbolic method, then justifies the existence of the livelock on the concrete machine by trace concretization in Section 4.2, by using SAT techniques that can handle large designs. The abstraction-based livelock checking is an incomplete method in the sense that it does not provide the proof of no livelock unless the checking is performed on a concrete machine. No livelock on an abstract machine does not guarantee no livelock on the concrete machine. However, the abstractionbased livelock checking enables finding real livelock errors on industrial large designs. 4.1
Let V be the set of state variables in an abstract machine for livelock checking. Suppose that R(V ) is the reached states in the abstract machine and L(V ) is a livelock group containing a TSCC. Also, suppose that v is a state variable in V . We are interested in whether v contributes to the livelock as in Definition 4. This is called variable causality.
Definition 4. When a livelock exists in the abstract machine, a variable v in V contributes to the livelock if the livelock disappears by eliminating v from the abstract machine. In other words, there is no livelock in another abstract machine that is composed of the variables, V \v.
Equation 1 shows a condition for existence of livelock.
L(V )
R(V )
Now, let R˜ be the quantified reached states and L˜ be the quantified livelock states with respect to a state variable v, as shown in Equation 2 and 3.
R~(V nv) = 9v: R(V )
L~(V nv) = 9v: L(V )
Then, it is determined by Equation 4 to check whether the variable v contributes to the livelock. Theorem 5 says that if Equation 4 holds, v contributes to the livelock.
L~(V nv)
R~(V nv)
Theorem 5. When a livelock group is found on an abstract machine (L(V ) ⊂ R(V )), if L˜(V \v) ⊂ R˜(V \v) holds for a variable v, the variable v contributes to the livelock.
Proof. Let M1 be the machine consisting of V and suppose that a livelock group exists in M1. Let M2 be the machine consisting of (V \v) by eliminating v from M1. Also, let T1 (T2) be the set of transitions in M1 (M2), respectively. Since M2 is an over-approximated machine from M1, M2 has more transitions than M1 (T1 ⊂ T2). Let Td be the difference between T1 and T2. If there is any transition (in Td) that makes a path from any state in the livelock to any state in the main group in M2, the livelock group merges into the main group and both groups become a single SCC, yielding L˜(V \v) = R˜(V \v). Thus, M2 becomes a machine without the livelock. This means that v is a necessary variable to have the livelock in M1. Therefore, if L˜(V \v) = R˜(V \v), v contributes to the livelock.
This causality checking can also be applied to a set of variables, especially with FSM variables, in order to report whether the livelocks are related with the FSM. Let F be the set of variables in an FSM and C be the set of variables in the COI of the FSM. Suppose that R(F; C) is the reached states in the abstract machine and L(F; C) is a livelock group containing a TSCC. The quantified reached states and the quantified livelock states are computed in Equation 5 and 6 with respect to the FSM variables, respectively.
R~(C) = 9F : R(F; C)
L~(C) = 9F : L(F; C)
Then, Equation 7 shows the causality checking with the FSM variables to check whether the FSM variables contribute to the livelock.
L~(C) = R~(C) 4.2
Once a livelock group is found on an abstract machine, we
need to justify whether the livelock group is reachable on the
concrete machine. This can be done by the following three
steps. The first step is to pick a target state in the livelock
group. The target state is chosen randomly from the livelock
group, but is one of the closest states to the initial states by
(1)
(2)
(3)
(4)
(5)
(6)
(7)
using the onion rings Ok in Figure 6. The second step is to
generate an abstract trace. Starting from the target state,
an abstract trace can be computed by applying BDD-based
pre-image computation iteratively until the initial state is
reached. The third step is to generate a concrete trace by
making a BMC (Bounded Model Checking [
Once a concrete trace is generated for a livelock group, the livelock is real on the concrete machine. We report the livelock group with the state classification mentioned in Section 3.1. A livelock group is reported with its initial state, the main group, transient group, and the unreachable states in terms of the number of states and the percentage in each group on the abstract machine.
By looking at the transient and livelock groups, we can see what fraction of the state space is in problematic zone. A good design is expected to have only one main group per one initial state without any transient and livelock groups, unless the design has an intended reset sequence to a normal mode. 5.
There is another important design property, called toggle deadlock that is related to livelock. A livelock may occur for multiple state variables of a design, whereas a toggle deadlock may occur on a single state variable. A state variable has a toggle deadlock if the variable initially toggles, but the variable gets stuck at a constant value after a certain number of cycles.
Figure 8 shows an example of toggle deadlock. There are two state variables {a; b} and four states {s0; s1; s2; s3} as in the example. Provided that s0 is the initial state, the main group is {s0; s1} and the livelock group is {s2; s3}. Once the state transition reaches to s2 that is a state in the livelock group, the value of b gets stuck at 1, whereas a still toggles. Thus, we say that b has a toggle deadlock.
a=0, b=0 s0 s1 a=1, b=0 a=0, b=1 s3 s2 a=1, b=1
Proof. To be a toggle deadlock, a variable is supposed to toggle at a cycle and to hold the value forever from the cycle. No STSCC implies that there is only main group in the design. If a variable appears as constant in the main group, the variable is a constant. However, the main group does not have any prefix behavior. This means it is not possible for the variable to get toggled before the main group. Therefore, no STSCC implies no toggle deadlock.
Theorem 6 shows that toggle deadlock occurs in the presence of a livelock. It is also possible that there is no toggle deadlock on a design that has a livelock. Thus, toggle deadlock on a state variable can be computed by two steps. First, D1 D2 Statistics
F D3-F1 D3-F2
COI 632 68
We have implemented the proposed livelock checking and toggle deadlock checking algorithms. Table 1 shows our experimental results on livelock and toggle deadlock checking, generated on a 1.4 GHz Intel processor machine with 4 GB memory running Red Hat Linux.
The first column lists the design names. The next five columns present the statistics on the designs, in terms of the number of latches (L), the number of inputs (I), the number of latches in FSM (F ), the number of toggle signals to check (T ), and the number of latches in the COI of either FSM and a toggle signal (COI). The next three columns show the results on livelock and toggle deadlock checking. The column with N shows how many latches were in the abstract machine. The column with Llk shows how many livelock groups are found and the column with Dlk shows how many toggle deadlock are found. The next six columns compare the performance between two methods (N ew1 and N ew2), in terms of time(T ime), memory(M em), and the number of image/pre-image computations(Ops). N ew1 is the proposed method without the trimming technique, whereas N ew2 is the proposed method with the trimming technique. The times are in the form of hh:mm:ss and the memory consumptions are in M-byte. The final two columns(T raceGen) show the results on trace generation on concrete machine for the livelock or toggle deadlock found by N ew2, and T ime shows the time spent for trace generation and Len shows the trace length.
We have chosen 3 industrial designs (D1, D2, and D3). For each design, we have run livelock or toggle deadlock checking on several sizes of abstract machines with the multiples of 30 latches. We have set the maximum run time to 24 CPU hours.
In D1, there is one FSM automatically extracted. The FSM consists of 7 latches and contains 632 latches in its COI. We can see that the run time is exponentially increased, depending on the size of the abstract machine. On this design, the livelock checking became infeasible when N =120.
In D2, there is also one FSM that was user-specified. The FSM consists of 25 latches and contains only 68 latches in its COI. This design has a livelock group. However, the livelock was not detected when N=30 and N=60. The livelock was detected only when all the latches in the COI were included in the abstract machine. In other words, the abstract machine is the concrete machine at the FSM point of view. Since the livelock was found on the concrete machine, trace concretization is not required since the abstract trace in Section 4.2 is already a concrete trace.
D2 is the only design showing a significant performance difference between N ew1 and N ew2 in the table. This is because this design has many transient states as well as many livelock groups. In this case, the trimming technique significantly reduced the number of image/pre-image operations from 386K to 70K (5.5X reduction) that gave big speed-up from 5 hours to 1 hour (5X speed-up). This shows that the trimming technique helps the performance when there are many transient states. When there is no transient states, the trimming technique becomes a pure overhead as shown in D3. However, the overhead is almost negligible from the experiment.
In D3, there are two FSMs (F 1 and F 2). F 1 is composed of 2 latches and a livelock was found with N =30 within 49 seconds. The livelock was justified by trace concretization that took 397 seconds, and the trace length was 66. F 2 is composed of 4 latches and a livelock was found with N =4 (the FSM itself) in 9 seconds. The livelock was also justified by trace concretization that took 114 seconds, and the trace length was 14. We have also tried the toggle deadlock checking on F 2 separately from the livelock checking. A toggle deadlock was found in 90 seconds and the concrete trace was generated in 131 seconds. D3 shows the value of abstraction-based livelock and toggle deadlock checking.
Table 2 shows a comparison on finding all SCCs with four
algorithms (XB [
Time
Memory 98.2 237.3 266.5 92.5
We have presented a framework for abstraction-based livelock and toggle deadlock checking, in order to handle large designs in practice. Since exact livelock and toggle deadlock checking is infeasible on real designs directly, our approach is to check livelock and toggle deadlock on abstract machine of either an FSM or a toggle signal. Once we find a livelock or toggle deadlock, we justify the livelock or toggle deadlock on the concrete machine by concretizing the abstract trace on the concrete machine.
Even though the proposed approach does not prove the non-existence of livelock or toggle deadlock on a design unless the design is small enough to handle, this approach finds livelocks or toggle deadlocks on the design if there exists.
To the best of our knowledge, it is the first approach to use the abstraction-based livelock checking and also the first approach for checking toggle deadlock. The experimental results showed that the abstraction-based approach finds livelock errors on the real designs.
As future work, we are interested in improving the concretization, finding more accurate influential latches, and optimizing the computations with multiple FSMs or toggle signals by considering the overlaps in their COIs.