Simulation is effective for checking expected design behaviour using selected test scenarios.
However, deadlock and progress-related problems can be difficult to expose when the required sequence is not included in the testbench.
Formal verification can help investigate these problems by exploring permitted input sequences and checking properties that describe progress.
What is a deadlock?
A deadlock occurs when a system reaches a state in which required progress cannot continue.
Consider a request-grant interface.
A requester raises req and expects the controller to eventually raise gnt.
If the controller enters an incorrect state and never grants the request, the system may stop making progress.
A simulation test may not expose this if it does not reach the problematic state.
Expressing progress requirements
A liveness property can describe the expectation that a request is eventually granted.
For example:
property p_req_eventually_granted; @(posedge clk) req |-> s_eventually gnt; endproperty assert property (p_req_eventually_granted);
This is an illustrative property. The exact syntax and support for s_eventually depend on the SystemVerilog language subset and formal engine.
The property also needs the correct protocol interpretation.
For example, it permits a grant in the same cycle as the request. If the protocol requires a later-cycle grant, the property must express that requirement instead.
Why fairness assumptions matter
A progress property may depend on the behaviour of the environment.
Consider an arbiter with multiple requesters. A request may not be granted if another requester continuously wins arbitration.
If the specification guarantees fairness, the verification model may need to represent the relevant fairness conditions.
However, fairness assumptions must come from the architecture or protocol specification. Adding them only to make a property pass can hide a genuine starvation problem.
Bounded response requirements
Some designs specify a maximum response time.
For example:
property p_bounded_grant; @(posedge clk) disable iff (!rst_n) req |-> ##[1:8] gnt; endproperty assert property (p_bounded_grant);
This property checks that a request is followed by a grant within one to eight clock cycles, subject to the reset and protocol semantics.
It is suitable only if the specification defines that response window.
What should be checked?
For deadlock and progress verification, engineers should consider:
- Requests that remain pending
- Arbitration fairness
- Resource dependencies
- Handshake completion
- State-machine transitions
- Reset recovery
- Timeout and retry behaviour
- Environmental conditions required for progress
Conclusion
Simulation can expose deadlocks when the relevant scenarios are exercised. Formal verification provides another way to explore permitted sequences and check whether progress requirements hold.
The key is to define the intended progress behaviour accurately and model environmental fairness conditions without hiding design defects.
