The AHAA Model: Structuring Formal Verification

Introduction

Formal verification succeeds when teams align tools, properties, and constraints with a clear verification intent. Many programmes struggle because they apply a single success criterion to every formal activity. Teams may expect exhaustive proof from early bring-up checks, or treat time-bounded runs as failures because tools do not converge.

The AHAA model provides a practical structure for deciding what formal verification should achieve at different stages of development. It separates verification work into four modes, each with distinct objectives, acceptable trade-offs, and completion criteria. This separation helps teams apply formal methods where they add value, without misinterpreting results or over-investing effort.

Five Key Learning Points

The AHAA Model for Formal Verification Decision-Making

What the AHAA model is and why it matters

The AHAA model divides formal verification activity into four distinct modes:

• Bug Avoidance: design practices, complexity analysis, interfaces, assertions, specification, RTL coding
• Bug Hunting: constrained-random, coverage, assertions, running applications, emulation or FPGA, post-silicon, software compatibility, formal
• Bug Absence: formal proofs for critical properties to achieve complete assurance
• Bug Analysis: debug practices, data analysis, and root cause analysis

Each mode answers a different verification question:

• Is the RTL fundamentally coherent and safe to build on?
• Can meaningful bugs be discovered quickly, even if completeness is not guaranteed?
• Which properties justify the cost of exhaustive proof?
• How can failures be reproduced, clustered, and fixed when they emerge late?

Treating these intents separately prevents wasted effort and misinterpretation of results. A time-bounded run that finds no failures can be a success in Bug Hunting. The same outcome is insufficient in Bug Absence, where proof under defined assumptions is required.

The figure below separates formal verification into four modes with distinct objectives and completion criteria. It illustrates why programmes should not apply a single success metric across all formal activities.

Figure 1: The AHAA model

Bug Avoidance: Fast Formal Feedback During RTL Bring-Up

Bug Avoidance supports design during RTL development and early feature integration. In many programmes, simulation testbenches mature later than early RTL changes. Formal checks, by contrast, can be deployed quickly to provide early structural feedback.

Bug Avoidance focuses on:

• Lightweight properties that confirm the RTL is not fundamentally broken
• Assumption checking at key integration boundaries
• Early bug capture using short counterexamples that simplify debugging

This mode works best when designers and verification engineers agree on a small set of “bring-up properties” that protect critical interfaces. These properties should remain simple and targeted. Bug Avoidance is not about exhaustive proof, but about reducing the likelihood that obvious defects propagate into later verification stages. Where appropriate, these checks are expressed using assertion-based methods. IEEE 1800 defines SystemVerilog Assertions, which remain the foundation of many industrial formal flows.

Bug Hunting: Time-Bounded Formal as a Search Engine

Bug Hunting treats formal verification as a focused search mechanism rather than a proof engine. The objective is to quickly discover meaningful bugs, even when runs are incomplete or have non-uniform durations. Success is measured by defect discovery efficiency, not convergence.

Figure 2: Bug Hunting applications and automation

Figure 2 illustrates a portfolio of automated bug-hunting applications commonly deployed in practice. These include X-propagation analysis, FSM structural checks, protocol compliance, clock-gating validation, system register access checks, and targeted coverage. Each application operates under a bounded time or a constrained scope, allowing teams to extract value early without incurring the cost of exhaustive proof.

By grouping these applications under a single intent, programmes avoid misinterpreting incomplete runs as failures. Instead, Bug Hunting is treated as an iterative process that continues until marginal bug discovery drops below an acceptable threshold.

Three practical principles define this mode:

• Bug Hunting does not require convergence
• Run times vary, and non-uniform runtimes are acceptable
• Runs should stop when failures stop appearing, because marginal value declines

Bug Hunting is low-cost and can start early. It targets bugs that simulation may miss at that stage, or finds them more quickly with simpler debugging.

This mode introduces challenges that teams must manage deliberately:

• False failures: selecting appropriate hierarchy levels to avoid wasted debug
• Non-exhaustive results: accepting partial runs because proof is not the objective
• Completion criterion: “no failures for the time available”, not “all proved”

A common optimisation is to convert proved properties into assumptions, reducing the cone of influence and accelerating subsequent checks.

Bug Absence: Exhaustive Proof for Critical Properties

Bug Absence applies when the programme requires complete assurance that a property can never be violated under defined constraints. In this mode, proof is the only acceptable outcome.

Typical targets include:

• Deadlock freedom
• Protocol compliance
• Security properties, such as preventing unauthorised register modification

Bug Absence introduces the strictest requirements:

• Complete and realistic environment constraints
• Careful use of hierarchy and abstraction
• Multiple proof engines and invariants, where required
• Clear completion criteria, defined as “proved” or “proved under stated conditions”

If a proof holds only under additional assumptions, teams must decide whether those assumptions reflect real operating conditions or mask defects. This mode demands the highest level of expertise and the most careful interpretation of results.

Bug Analysis: Formal as a Debug and Fix Validation Tool

Bug Analysis focuses on the investigation around a specific failure, particularly bugs that are difficult to reproduce.

Typical tasks include:

• Reproducing bug conditions
• Clustering similar failures
• Validating fixes and checking for regressions
• Investigating silicon bugs by encoding observed behaviour into formal constraints

This mode often becomes critical late in a programme, when failures arise from rare combinations of sequencing, concurrency, and software interaction. Formal tools can explore paths that simulation cannot reach economically, provided the environment is modelled accurately.

Concrete Examples of AHAA in Practice

A range of practical applications maps naturally to the AHAA modes and demonstrates how the model translates into repeatable verification flows:

• Protocols: certifying compliance with AXI, ACE, AHB, ATB, and APB using formal-optimised checkers
• X-propagation: detecting and debugging X issues using mostly auto-generated properties
• Finite State Machines: generating reachability and transition-conformity properties from textual specifications
• Clock gating: verifying enable conditions, register stability, and input sampling
• Sequential equivalence checking: proving functional equivalence across design mutations
• System registers: using a common register description reference (ART) to generate assertions and improve exhaustiveness
• Coverage: identifying dead code and validating that constraints do not over-restrict behaviour

These examples reinforce a strategic principle: formal verification should be treated as a portfolio of intent-aligned applications rather than a single monolithic activity.

Figure 3: System register checking using a common description reference (ART)

Figure 3 shows a structured flow from register descriptions to assertion generation, RTL checks, and formal analysis. It illustrates how shared artefacts reduce manual effort and improve exhaustiveness for register access properties.

Conclusion

The AHAA model provides a practical way to align formal verification effort with programme intent. By separating bring-up checks, time-bounded bug discovery, exhaustive proof, and late-stage debug into distinct modes with different success criteria, teams reduce wasted effort and improve confidence in results.

When adopted deliberately, this structure allows formal verification to function as a strategic capability across the RTL-to-silicon lifecycle, rather than a source of friction or misunderstanding.

Continue Exploring

If you would like to explore more work in this area, see the related articles in the
Verification section on the Alpinum website:
https://alpinumconsulting.com/resources/blogs/verification/

For discussion, collaboration, or technical engagement, contact Alpinum Consulting here:
https://alpinumconsulting.com/contact-us/

References

[1] Alpinum Systems Ltd., AHAA Model for Formal Verification, internal methodology. https://alpinumconsulting.com/

[2] IEEE, IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language (IEEE 1800). https://ieeexplore.ieee.org/document/10458102

[3] Design and Verification Conference (DVCon), formal verification usage patterns. https://dvcon.org/

[4] ISO 26262 and related safety-critical verification case studies. https://www.iso.org/standard/68383.html