Why Deadlock and Livelock Bugs escape Simulation in Modern SoC Interconnects
Modern SoCs can pass thousands of functional tests and still fail because the system stops making progress. Deadlocks in SoC designs rarely trigger a protocol violation or produce an incorrect value. Instead, a valid request may never complete, a response may never return, a credit may never be released, or an arbiter may continue moving traffic while one critical transaction is permanently blocked. These are forward-progress failures. They include deadlock, livelock, and starvation. They are difficult to expose with simulation because they often depend on rare combinations of internal state, backpressure, arbitration decisions, routing dependencies, queue occupancy, protocol ordering, and timing alignment.
Formal verification changes the question. Instead of asking whether a particular simulation test exposed a hang, formal methods can ask whether a hang condition is reachable under a defined set of assumptions. This makes formal verification highly relevant for AXI fabrics, NoCs, cache-coherent paths, DMA subsystems, request/grant logic, arbitration logic, credit-based flow control, and control-heavy FSMs.
This blog explains why deadlocks in SoC interconnects escape simulation, where these bugs appear in modern designs, and how formal verification can provide stronger evidence for forward-progress sign-off.
Why deadlocks in SoC designs are a forward-progress risk
A system is not fully verified simply because it produces correct outputs in the scenarios exercised. It must also continue to make progress. Modern SoCs contain processors, accelerators, DMA engines, caches, coherent fabrics, memory controllers, protocol bridges, security blocks, and peripheral subsystems. These components share resources and communicate through layered interconnect structures. Each block may be correct locally, and each interface may follow its protocol rules, but the complete system can still enter a state where useful work cannot be completed.
For example, a CPU may issue a valid memory request. A DMA engine may follow its descriptor protocol. An accelerator may generate legal traffic. The interconnect may preserve local handshake rules. Yet a rare dependency cycle can still prevent completion if one resource waits for another resource that can never become available.
This is the essence of forward-progress risk. The failure is not necessarily an illegal local transition. It is the inability of the composed system to complete the required work. The routing literature has recognized this problem for decades. Dally and Seitz showed that a deadlock-free routing algorithm for an interconnection network depends on the absence of cycles in the channel dependency graph, and that virtual channels can be used to remove dependency cycles [1].
Deadlock, livelock, and starvation: the difference
A deadlock occurs when two or more processes, agents, channels, or resources are mutually blocked. Each is waiting for another condition that cannot occur because the system has entered a circular dependency.
A livelock occurs when the system continues to change state, but no useful work is completed. Activity is visible, but the transaction, packet, request, or operation of interest does not terminate.
Starvation occurs when one request, traffic class, master, or agent is repeatedly denied the resource it needs, even though the rest of the system continues to operate.
The Qualcomm/Oski DVCon presentation defines these three failure modes in the context of system-level deadlock verification. It describes deadlock as cyclical dependency and mutual blocking between processes, livelock as apparent progress without termination, and starvation as a process failing to receive the required resource because it repeatedly loses competition for shared resources [2].
This distinction matters because each failure mode needs a different verification strategy. A deadlock proof may focus on circular wait and resource dependency. A livelock proof may need to show eventual completion. A starvation proof may require assumptions of fairness, bounded service, or arbitration.
Why simulation struggles to expose deadlocks in SoC interconnects
Simulation is essential for functional verification, but detecting deadlocks in SoC designs depends entirely on the scenarios exercised. A simulation test can expose a deadlock or livelock only if it creates the right traffic pattern, reaches the right internal state, fills the right queues, triggers the right arbitration sequence, and aligns the right backpressure condition at the right time.
This is difficult because forward-progress bugs often emerge from the interaction of legal local behaviors. No single local interface may be doing something obviously wrong. The failure appears only when multiple agents, queues, channels, or control states interact in a rare combination.
The Qualcomm/Oski DVCon paper explains that SoC teams traditionally rely on RTL simulation and emulation for system-level requirements such as safety, security, coherency, and the absence of deadlock, but subtle system-level bugs can slip through because corner-case coverage remains low in complex designs [3]. Arm/Mentor material on advanced formal deadlock verification makes a similar point. It describes deadlocks, livelocks, and QoS issues as some of the most difficult hardware bugs to find, and explains that watchdog-based simulation or emulation techniques are not exhaustive [4].
The issue is not that simulation has no value. The issue is that simulation can only demonstrate the behavior it exercises. For forward-progress bugs, the hardest cases may sit in the unvisited space between legal local behavior, rare timing alignment, and system-level dependency.
Where these bugs appear in SoC interconnects and control fabrics
Livelocks and Deadlocks in SoC designs are most likely to appear where control, buffering, and arbitration interact.
These areas are strong candidates for formal verification because the risk is often control-heavy rather than datapath-heavy. A bug may depend less on the value of a wide data bus and more on whether a request, grant, credit, response, retry, or state transition eventually occurs.
The Qualcomm/Oski paper notes that control-oriented problems, such as system-level deadlock, are suitable targets for formal verification, but also explains that full-system RTL proofs can be difficult because of design complexity. This motivates architectural formal modeling and abstraction [3].
How formal verification changes the problem
Simulation usually asks:
Did this scenario work?
Formal verification can ask a stronger question:
Can this failure happen under the stated assumptions?
For forward-progress verification, that difference is powerful. Formal properties can express obligations such as:
- If a valid request is accepted, a response must eventually be returned.
- If a request remains asserted, a grant must eventually occur.
- If a packet enters a fabric, it must eventually leave or reach its destination.
- If a credit is consumed, it must eventually be returned.
- If an FSM enters a valid operating state, it must not remain permanently stuck.
- If traffic is blocked, the blockage must be bounded or recoverable.
A DVCon paper on forward-progress checks explains that formal verification can be used to analyze and prove forward progress using safety and liveness assertions, with case studies showing critical issues found in designs [5]. For readers who want the property-level background, LUBIS EDA’s guide to safety and liveness properties explains why “nothing bad happens” properties and “something good eventually happens” properties are both important in formal verification [6].
This does not mean formal verification is automatic. Progress proofs can be harder than local safety checks. They require careful property writing, assumption review, fairness handling, proof bounds, abstraction, and debug discipline. However, when the proof is properly scoped and converges, the result is stronger than a passing test. It shows that the failure condition is not reachable within the defined proof context.
Architectural formal verification for system-level deadlocks
Full RTL formal verification of a system-level progress issue is often infeasible when attempted directly. The challenge is not only state-space size, but also the level of design detail being analyzed. A deadlock scenario may depend on control movement, resource ownership, dependency cycles, buffer availability, and completion obligations. It usually does not require every datapath value, payload bit, or implementation detail to be modeled.
This is where architectural modeling becomes useful. Instead of proving the property directly on the full RTL system, engineers can build abstract models that preserve the progress-relevant behavior of each block. These models capture how resources are requested, held, released, and passed between blocks, while removing implementation detail that does not affect the deadlock question.
The Qualcomm/Oski DVCon paper describes an architectural formal verification process for system-level deadlocks. The approach uses architectural models to verify system-level requirements and presents an industrial case study where the methodology was used to verify the absence of deadlocks [3].
The corresponding presentation summarizes the methodology in three steps [2]:
- Develop architectural models for the blocks in the system.
- Formally verify the system of block-level architectural models.
- Validate block architectural models against RTL.
This approach separates the system-level progress question from unnecessary implementation detail. For deadlock verification, the model needs to preserve the relevant resource dependencies and progress behavior. It does not always need to preserve a full datapath implementation. The Qualcomm/Oski presentation also reports use in a wireless SoC PHY subsystem, where the methodology demonstrated the absence of deadlocks and identified nine difficult bugs that could have caused performance issues or an unplanned respin if left undiscovered [2].
Figure 4 shows a three-step architectural formal approach: architectural specifications are converted into abstract models, the interacting model system is formally verified for progress, and each model is then validated against RTL. This preserves the key dependency behavior needed for system-level deadlock analysis while avoiding unnecessary RTL detail.
Why local protocol correctness does not guarantee system-level progress
Architectural models are only useful if they preserve the behavior that matters for progress. In deadlock and livelock verification, that behavior is not limited to whether each interface follows its local protocol. The more important question is how requests, responses, credits, buffers, grants, and resources depend on one another across the system.
This is a key reason why deadlocks in SoC systems cannot be ruled out by local checks alone. A local protocol check may verify that an interface adheres its handshake rules. A FIFO may correctly implement push and pop behavior. An arbiter may follow its programmed priority scheme. A bridge may preserve legal request and response signaling. Each of these checks is necessary, but none of them alone proves that the composed system will always make progress.
Forward-progress bugs are often compositional. They emerge when legal local behaviors interact in an unsafe global dependency pattern.
For example:
- Master A waits for a response from Interconnect B.
- Interconnect B waits for buffer space in Bridge C.
- Bridge C waits for a credit or completion that depends on Master A’s path moving first.
Every local wait may be legal. The global dependency is not. This is why progress verification must combine local checks with system-level reasoning. Local protocol checks are necessary, but the verification plan must also ask whether accepted requests are completed, whether resources are eventually released, and whether legal traffic can create a circular wait.
The classic channel dependency graph result from Dally and Seitz captures this principle in the context of interconnection networks: absence of cycles in the dependency graph is central to deadlock-free routing [1]. Modern SoC fabrics and NoCs have additional protocol layers and design-specific complexity, but the same underlying risk remains: legal local dependencies can compose into a global progress failure.
Figure 5 shows that local connectivity does not by itself prove system-level progress. Deadlock depends on the dependency graph created by routing and channel usage. Dally and Seitz show how adding virtual edges/channels can break dependency cycles and support deadlock-free routing. Source: Dally and Seitz [1].
Debugging forward-progress counterexamples
Debugging a forward-progress failure is different from debugging a simple safety violation. A safety counterexample often shows a direct illegal event. A deadlock or livelock counterexample may show many legal events that eventually lead to no useful progress. The design may not “break” in a single obvious cycle. Instead, it may slowly enter a circular wait, an unfair arbitration pattern, a blocked credit condition, or a non-exiting control sequence.
Effective debugging should answer:
- Which request, packet, credit, or resource stopped progressing?
- What was the first blocking condition?
- Which dependency chain followed?
- Which block or state held the resource needed by another block?
- Did the failure depend on invalid environment behavior?
- Was an assumption missing, too weak, or too strong?
- Is the counterexample a real RTL bug, a modeling issue, or an incomplete specification?
- Can the failure be turned into a reusable regression property?
This is where structured Assertion IP and formal methodology matter. A good progress property should not only fail; it should fail in a way that helps engineers identify the blocking mechanism. Arm/Mentor’s published material emphasizes that deadlock debug is one of the difficult parts of the problem and discusses formal-based approaches that either find show-stopper bugs or prove the absence of deadlock under all time and input conditions [4], [8].
For project teams, the practical value is clear. A reproducible counterexample can shorten debugging time, support design review, and serve as a regression artifact that prevents the same progress bug from recurring in a later RTL revision.
What a forward-progress verification plan should include
Deadlock and livelock verification should not start with random assertions. It should start with a progress model. A strong plan defines what must be completed, which resources can block, which dependencies matter, what the environment is allowed to do, and which proof outcomes are needed for sign-off.
This structure turns progress verification into an engineering argument rather than a tool experiment. It also avoids two common problems: writing properties that are too local to catch system-level progress bugs, or writing global progress properties that are too broad to converge.
LUBIS EDA’s blog on abstraction methodology explains that signal-cutting and black-boxing can reduce proof complexity by narrowing the cone of influence, but they require careful constraints or auxiliary logic to prevent false counterexamples [7]. This is particularly relevant to forward-progress verification, where the proof must preserve the dependency behavior that matters while removing irrelevant implementation details.
How LUBIS EDA can support this problem
Deadlock and livelock verification requires more than a formal tool. It requires property planning, abstraction, assumption review, proof execution, counterexample interpretation, regression integration, and sign-off documentation. This aligns with LUBIS EDA’s formal verification service model. LUBIS EDA positions formal sign-off around finding simulation-resistant bugs, creating a formal sign-off plan, defining assumptions and constraints, tracking coverage and convergence, delivering sign-off reports, and providing reusable artifacts [9].
For forward-progress verification, LUBIS EDA can support customers in several practical ways:
Conclusion: Functional correctness is not enough if the system cannot make progress
Deadlock, livelock, and starvation bugs expose a critical weakness in simulation-heavy verification strategies. A design can pass many functional tests and still fail because a valid transaction never completes. These bugs are difficult because they often sit above local protocol correctness. Each block may behave legally, but the system may still enter a circular dependency, an unfair arbitration pattern, an unreleased credit condition, or a non-terminating control sequence.
Formal verification changes the verification question. Instead of waiting for a test to hit the right combination of traffic and timing, formal methods can ask whether a progress failure is reachable under defined assumptions. For modern SoC interconnects, NoCs, AXI fabrics, cache-coherent paths, DMA subsystems, request/grant logic, arbitration logic, and control-heavy IP, this capability is increasingly important.
The strongest progress-verification strategy combines local protocol properties, system-level progress obligations, cover checks, abstraction, assumption review, architectural modeling, counterexample debug, and regression tracking. It also requires a delivery model that turns proof activity into usable sign-off evidence.
Functional correctness is necessary. It is not sufficient. A system that computes correctly only when it continues moving is not fully verified until forward progress has been addressed.
References
[1] W. J. Dally and C. L. Seitz, “Deadlock-Free Message Routing in Multiprocessor Interconnection Networks,” IEEE Transactions on Computers, vol. C-36, no. 5, pp. 547–553, May 1987. Available:https://authors.library.caltech.edu/records/fd0yr-br438
[2] M. Munishwar and V. Singhal, “Architectural Formal Verification of System-Level Deadlocks,” DVCon presentation, Qualcomm Atheros and Oski Technology, 2018. Available: https://dvcon-proceedings.org/document/architectural-formal-verification-of-system-level-deadlocks-presentation/
[3] M. Munishwar, N. Zaman, A. Jain, H. Singh, and V. Singhal, “Architectural Formal Verification of System-Level Deadlocks,” DVCon U.S., 2018. Available: https://dvcon-proceedings.org/wp-content/uploads/architectural-formal-verification-of-system-level-deadlocks.pdf
[4] L. Arditi, V. Abikhattar, A. Ali, and J. Hupcey III, “Easy Deadlock Verification and Debug with Advanced Formal,” Arm/Mentor DAC 2020 material. Available: https://codasip.com/wp-content/uploads/dlm_uploads/2023/09/DAC2020-extended-version.pdf
[5] A. Garg, “Forward Progress Checks in Formal Verification: Liveness vs Safety,” DVCon U.S., 2024. Available:https://dvcon-proceedings.org/document/forward-progress-checks-in-formal-verification-liveness-vs-safety/
[6] LUBIS EDA, “Safety vs Liveness Properties in Formal Verification,” 2024. Available: https://lubis-eda.com/safety-vs-liveness-properties-in-formal-verification/
[7] LUBIS EDA, “Abstraction Techniques in Formal Verification,” 2024. Available: https://lubis-eda.com/formal-verification-abstraction-methodologies/
[8] Siemens Verification Horizons, “DAC 2020 Paper Report: Easy Deadlock Verification and Debug with Advanced Formal Verification,” Aug. 2020. Available: https://blogs.sw.siemens.com/verificationhorizons/2020/08/04/dac-2020-paper-report-easy-deadlock-verification-and-debug-with-advanced-formal-verification/
[9] LUBIS EDA, “Formal Verification Sign-Off as a Service.” Available: https://lubis-eda.com/services/
[10] LUBIS EDA, “FormalOS: Formal Verification Platform for Sign-Off Delivery,” 2026. Available: https://lubis-eda.com/formalos/