When Formal Proofs Do Not Converge: Diagnosing Unproven Properties, Bounded Results and Proof Complexity

When a formal property neither produces a valid counterexample nor reaches a complete proof, the result is unresolved. An Unproven result is therefore neither a pass nor automatically evidence of defective RTL. The first task is to validate the requirement, property, environment, reset and reachability. Only then should engineers reduce proof complexity, add invariants, introduce abstraction or adjust engines and resources. Any bounded evidence must be reported with its exact model, assumptions, scope and depth.

What Does It Mean When a Formal Proof Does Not Converge?

Formal property checking asks whether a specified property holds for the behaviours represented by a particular model. A completed proof is therefore conditional: the property must express the intended requirement, the RTL configuration and reset model must be appropriate, environmental assumptions must be realistic, and any abstractions must preserve the claim being made.

IEEE 1800-2023 defines the semantics of SystemVerilog, including its assertion and coverage constructs, while Accellera material describes SystemVerilog Assertions (SVA) as a core mechanism for assertion-based and formal verification. Property semantics including sampling are consequently part of the verification problem, not merely syntax. [1][2]

“Non-convergence” is useful engineering shorthand, but it does not identify a root cause. The difficulty may lie in the assertion, environment, analysed design scope or computational problem. A timeout alone cannot distinguish them.

Proven, Falsified, Bounded and Unproven Results

Formal tools do not use identical result taxonomies. Terms such as Proven, Pass, Failed, Falsified, Bounded, Inconclusive, Unproven and Unknown can have tool- and engine-specific meanings. Cadence, for example, documents lower, upper and bounded proof information in Jasper, while Siemens material uses inconclusive when analysis cannot resolve the problem within available capacity. [3][4]

Formal Result Classification and Required Action

Not every tool reports every category separately. Vacuity and unreachability may also be secondary diagnostics rather than top-level property statuses.

Why Formal Proofs Fail to Converge

State-space size matters, but “state-space explosion” is not an adequate diagnosis. An assertion may be difficult because it depends on long sequential history, arbitration, counters, memories or many interacting state elements. It may also be difficult because the formal environment admits behaviour that real hardware never sees, or because the property itself is unnecessarily complex.

The DVCon bounded-proof study identifies large sequential cones of influence, arbiters, counters, memories, FIFOs, assumptions and assertion models among practical sources of difficult proofs. [5]

Why a Formal Property May Remain Unproven

Symptoms are clues, not proofs of root cause.

Property Problems vs Proof-Complexity Problems

A useful separation is:

• Property problem: the assertion does not encode the requirement cleanly, has incorrect sampling or temporal semantics, or contains unnecessary complexity.
• Environment problem: reset, initial state, assumptions or constraints do not represent legal operation.
• Scope problem: too much irrelevant logic or state participates in the obligation.
• Proof-complexity problem: the claim and environment are legitimate, but the resulting state/transition problem remains hard.

This order matters. Solver tuning cannot repair a wrong requirement.

Formal Proof Non-Convergence Decision Tree

Use a gated diagnostic sequence rather than immediately modifying proof options:

1. Confirm the requirement
2. Confirm that the property encodes the requirement
3. Check compilation, clocking and sampling semantics
4. Validate reset and initial-state modelling
5. Review assumptions and constraints
6. Demonstrate meaningful activation and reachability
7. Inspect the property’s cone of influence and sequential depth
8. Decide whether justified partitioning, abstraction or invariants can reduce complexity
9. Review proof engines, bounds and computational resources
10. Re-run and classify the evidence
11. Decide whether simulation or system-level evidence is required
12. Record the unresolved limitation and responsible reviewer

The sequence is deliberately front-loaded with verification-intent checks. Tool-specific workflows may differ.

Validate the Requirement and Property First

Before changing assumptions or abstractions, read the requirement and assertion together. Check implication direction, temporal ranges, overlapping versus non-overlapping behaviour, disable/reset conditions, clocks and sampling.

For a request/acknowledge property, for example, “an acknowledgement follows a request within four cycles” is different from “if a request is sampled, acknowledgement occurs one to four sampled clock events later”. The engineering requirement must decide which formulation is correct.

Safety properties normally describe behaviour that must never occur; a violation has a finite witness. Liveness properties express eventual progress and may require explicit fairness or progress reasoning. Treating an eventual-grant property like a short bounded safety check can produce misleading confidence. [6]

Check Assumptions, Constraints, Reset and Reachability

Assumptions define which environments the proof is allowed to consider. Under-constraint can admit impossible traffic and make the proof unnecessarily difficult or produce irrelevant failures. Over-constraint can remove legal behaviour and make an invalid engineering claim appear easy to prove. Do not strengthen assumptions merely because a property is difficult.

Use cover properties or another witness mechanism to demonstrate that important antecedents, modes and corner-case sequences can occur. Reset deserves explicit review: an unrealistic initial state may create artificial complexity, while an over-restrictive reset model may remove behaviour that should have been analysed.

For a deeper discussion of misleading green results, see Alpinum’s analysis of vacuity, over-constraint and unreachable properties.

Analyse the Cone of Influence and Sequential Depth

The cone of influence (COI) identifies logic capable of affecting the property, directly or through its assumptions and dependencies. Siemens recommends examining the active COI when an analysis becomes inconclusive. [4]

Distinguish structural width from temporal depth. A relatively small controller can still require deep reasoning if progress depends on queues, backpressure or repeated arbitration. Conversely, a wide datapath may admit a compact abstraction. A numerical proof depth is not a universal measure of verification progress. One hundred clock events may cover many meaningful transactions for one protocol and barely initialise another design.

Reduce Proof Scope Without Changing the Claim

Safe scope reduction keeps the engineering statement intact.

Useful options include:

• Splitting an end-to-end requirement into interface or pipeline obligations
• Proving independently reusable sub-block contracts
• Removing logic that cannot affect the property
• Tracking a representative symbolic transaction rather than every datapath value
• Isolating control logic from irrelevant datapath implementation

The DVCon bounded-proof case study describes breaking large end-to-end assertions into smaller obligations and verifying some submodules separately before using abstractions. That is one project methodology, not a universal sign-off rule. [5]

Use Abstraction Without Creating False Confidence

Abstraction trades implementation detail for a smaller verification problem. The trade must be explicit.

Counterexample-guided abstraction-refinement research demonstrates the central risk: an abstract model may admit spurious counterexamples, requiring refinement before the trace can be treated as a real design failure. [7]

Likewise, Siemens’ memory-abstraction guidance notes that black-boxed outputs become free inputs, so resulting failures require investigation to determine whether the abstraction created them. [8]

Partition the Design and Apply Assume-Guarantee Reasoning

Assume-guarantee reasoning decomposes a system-level obligation into component guarantees under explicit environmental assumptions. It can reduce the state space dramatically, but the component assumptions must eventually be justified by the neighbouring components or system context. Research on compositional verification emphasises that this reasoning requires a sound method for discharging assumptions; circular “A works if B works, and B works if A works” arguments cannot simply be accepted. [9]

Add Invariants, Lemmas and Helper Properties

Induction may fail because the inductive hypothesis admits mathematically possible states that are unreachable in the real design. An invariant can capture a necessary fact for example, FIFO occupancy never exceeds its implemented capacity. A helper lemma can establish an intermediate relationship between pipeline stages or protocol phases.

The important distinction is whether the helper fact is proved or merely assumed. A proved lemma strengthens the reasoning chain. An assumed lemma transfers part of the proof obligation into the environment and therefore requires separate justification.

Review Proof Engines, Bounds and Computational Resources

Only after validating intent, environment and proof structure should engineers optimize engine selection, orchestration, run limits or compute allocation. Different proof strategies suit different structures, and current commercial platforms use portfolios of engines and orchestration. Their result terminology and bound semantics vary, so tool documentation should determine exactly what a reported bound means.

Engineers who want structured practice across properties, constraints, proof analysis and unresolved-result diagnosis can develop practical formal proof and debug skills through Alpinum’s hardware-focused programme.

How to Interpret a Bounded Formal Result

Bounded model checking analyses behaviour only to a defined bound; classic SAT-based BMC literature formalises this as searching for counterexamples up to a maximum length. [10]

A safer engineering statement is:

A bounded analysis may establish that no counterexample exists within the analysed depth, under the model, assumptions, initial-state semantics and property interpretation used by the tool.

It should not be rewritten as “the design is correct for N cycles”.

The meaning of depth depends on:

• The temporal structure of the property
• Reset and initial-state semantics
• Environmental assumptions
• Design configuration
• Proof method and tool semantics
• Actual functional latency

A depth of 100 may be substantial for a fixed four-cycle request/response rule. The same depth may be weak evidence for a long queue under backpressure, a fairness-dependent arbiter or an eventual-progress requirement. Increasing a bound adds explored depth; it does not by itself turn the result into an unbounded proof.

When Bounded Evidence Is Useful and When It Is Not

Bounded evidence can be useful when the relevant functional horizon can be justified independently for example, when architectural latency, cover witnesses, corner-case sequencing and complementary verification establish why a particular depth is meaningful.

The 2021 DVCon study presents one such project-specific methodology combining calculated latency, scenario covers and formal coverage for packet-processing logic. Its own case study also exposed a reset-abstraction issue during coverage analysis, illustrating why the bound itself was not enough. [5]

It is weak evidence when the required horizon is unknown, progress depends on unbounded waiting, important modes are unreachable, or the result depends on poorly validated abstraction.

Combine Formal Results with Simulation and Coverage

Formal and simulation answer different verification questions. Simulation is often better suited to realistic workloads, long software-driven scenarios, performance behaviour and complex system interactions. Formal is powerful where a precise property and tractable model permit exhaustive reasoning over the relevant state space.

Alpinum’s verification planning and coverage-closure guidance similarly treats formal and simulation as complementary rather than interchangeable.

Code coverage is not proof of completeness. Formal coverage can expose reachability, observability or proof-core gaps, but high coverage does not automatically make the requirement set complete or the sign-off decision correct. The DVCon bounded-proof study explicitly combines coverage information with engineering analysis rather than treating the metric alone as proof. [5]

Mutation or fault-based qualification can add another perspective by asking whether deliberately introduced behavioural changes are detected by the property set. It tests checker effectiveness; it still cannot establish that every intended requirement was specified correctly. DVCon Europe work on mutation coverage makes the same distinction between activation and observation of functional effects. [11]

Formal Sign-Off When Properties Remain Unproven

Formal sign-off is an engineering governance decision, not a colour on a dashboard. Criteria vary by programme, application, risk and verification plan.

Formal Sign-Off Decision Matrix

No row automatically authorises tape-out. The responsible project stakeholders must define and approve sign-off criteria.

Where a programme needs external delivery support rather than education, Alpinum separately describes its formal verification services for ASIC and SoC development.

Proof-Convergence Checklist

Before changing an unresolved property’s status, confirm that:

• Requirement reviewed and uniquely identified
• Property reviewed against that requirement
• Clocking and sampling semantics checked
• Reset and initial-state model checked
• Assumptions reviewed against legal operation
• Under-constraint and over-constraint considered
• Cover/witness demonstrates meaningful activation
• Cone of influence understood
• Proof complexity classified
• Invariants and lemmas are justified or independently proved
• Abstractions are documented and validated
• Partition boundaries and interface contracts are reviewed
• Tool settings and engine strategy are recorded
• Achieved proof bound and its semantics are recorded
• Relevant formal coverage has been reviewed
• Complementary simulation evidence is linked
• Residual uncertainty is written explicitly
• Responsible technical reviewer is identified
• Final result classification is approved

The wider AHAA formal-verification framework provides useful context: bounded bug hunting and proof-oriented bug absence deliberately have different completion criteria.

Key Takeaways

A non-convergent property is a diagnostic problem before it is a computational problem.

Validate the requirement, assertion semantics, reset, assumptions and reachability before manipulating proof scope. Then inspect the COI and sequential depth, and introduce decomposition, abstraction or invariants only with explicit evidence that the engineering claim remains valid. Treat bounded results as precisely scoped evidence. Treat abstractions as new proof obligations. Combine formal results with simulation and coverage where they answer complementary questions. Most importantly, record unresolved uncertainty rather than translating it into a pass.

For engineers building this capability hands-on, Alpinum’s six-day practical formal-verification programme covers property writing, proof analysis, debug, formal coverage and advanced proof techniques.

References

[1] IEEE, IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language, IEEE Std 1800-2023, Feb. 2024, doi: 10.1109/IEEESTD.2024.10458102.
https://ieeexplore.ieee.org/document/10458102

[2] I. Ciocirîan, A. Radu, R. Calderón-Rico, and I. Tapia, “SVA advanced topics: SVAUnit and assertions for formal,” tutorial presented at DVCon U.S. 2016, San Jose, CA, USA, Feb. 29, 2016. https://www.accellera.org/resources/videos/systemverilog-assertions-tutorial-2016

[3] A. Anand, C. Chen, B. N. Subramanian, and J. Hupcey, “‘Bounded Proof’ sign-off with formal coverage,” in Proc. Design and Verification Conference and Exhibition (DVCon U.S.), 2021. https://dvcon-proceedings.org/wp-content/uploads/bounded-proof-sign-off-with-formal-coverage.pdf

[4] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, “Symbolic model checking without BDDs,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 1579, Berlin, Germany: Springer, 1999, pp. 193–207, doi: 10.1007/3-540-49059-0_14. https://doi.org/10.1007/3-540-49059-0_14

[5] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement for symbolic model checking,” Journal of the ACM, vol. 50, no. 5, pp. 752–794, Sep. 2003, doi: 10.1145/876638.876643. https://doi.org/10.1145/876638.876643

[6] T. A. Henzinger, S. Qadeer, and S. K. Rajamani, “You assume, we guarantee: Methodology and case studies,” in Proc. 10th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1427, Vancouver, BC, Canada, 1998, pp. 440–451, doi: 10.1007/BFb0028765. https://doi.org/10.1007/BFb0028765

[7] J. Hupcey III, “How to reduce the complexity of formal analysis—Part 1: Finding where formal got stuck and some initial corrective steps to take,” Siemens Verification Horizons, Aug. 8, 2018. [Online]. https://blogs.sw.siemens.com/verificationhorizons/2018/08/08/how-to-reduce-the-complexity-of-formal-analysis-part-1-finding-where-formal-got-stuck-and-some-initial-corrective-steps-to-take/

[8] J. Hupcey III, “How to reduce the complexity of formal analysis—Part 3: Assertion decomposition,” Siemens Verification Horizons, Sep. 11, 2018. [Online].
Siemens Assertion Decomposition, Part 3

[9] J. Hupcey III, “How to reduce the complexity of formal analysis Part 5: Memory abstraction,” Siemens Verification Horizons, Oct. 23, 2018. [Online]. https://blogs.sw.siemens.com/verificationhorizons/2018/10/23/how-to-reduce-the-complexity-of-formal-analysis-part-5-memory-abstraction/

[10] Cadence Design Systems, “Bounded proofs, lower bounds, and upper bounds in Jasper Formal Property Verification,” Cadence Support, Application Note, May 23, 2024. [Online]. https://support1.cadence.com/public/docs/content/20513928.html

[11] H. Busch, “An efficient methodology for mutation-coverage-collection of formal-property-checking,” in Proc. Design and Verification Conference and Exhibition Europe (DVCon Europe), Munich, Germany, Dec. 6–7, 2022. https://dvcon-proceedings.org/wp-content/uploads/75412.pdf

FAQs