Using Formal Verification for ISO 26262 Safety Compliance in Automotive Semiconductor Design

Originally published on Alpinum Consulting website

Introduction

Automotive semiconductor design operates under sustained pressure to ensure functional safety. Advanced driver assistance systems, domain controllers, and electrified powertrains demand increasingly complex SoCs that often integrate heterogeneous compute clusters, accelerators, safety monitors, and secure communication fabrics.

ISO 26262 defines a structured framework for functional safety in road vehicles. However, as integration density increases, conventional simulation-based verification struggles to provide the level of confidence required for higher Automotive Safety Integrity Levels (ASILs).

Formal verification for ISO 26262 safety compliance provides a complementary mechanism. Rather than relying solely on stimulus-based testing, formal methods reason about all reachable states within defined constraints. This enables proof-based assurance for critical safety properties, particularly in control logic and fault-handling mechanisms.

Five Key Learning Points

ISO 26262 Verification Requirements

ISO 26262 defines structured verification and validation activities across the safety lifecycle. For semiconductor development, the most relevant parts are:

• Part 4 – Product development at the system level
• Part 5 – Product development at the hardware level
• Part 6 – Product development at the software level

Part 5 specifies requirements for hardware safety development and verification, including the implementation of safety mechanisms, architectural metrics, and hardware integration verification.

Across these parts, ISO 26262 emphasises:

• Traceability from safety goals to technical safety requirements
• Verification of safety mechanisms
• Demonstration of freedom from interference
• Objective confirmation measures
• ASIL-dependent rigour and evidence expectations
• Verification must demonstrate that safety requirements are implemented correctly and operate as intended across defined operational modes and lifecycle states.

Crucially, ISO 26262 does not prescribe specific tools. Instead, it requires objective evidence and methodological rigour. This creates a natural alignment with formal verification, which can provide proof-based evidence for safety-critical properties.

Figure 1: ISO 26262 lifecycle mapped to formal verification. Source: byhon.it

Figure 1 shows the ISO 26262 safety lifecycle from item definition through production and operation. Formal verification activities align primarily with hardware development (Part 5), system integration, and confirmation measures, where proof-based evidence contributes directly to the safety case.

Formal methods can support:

• Derivation of formal properties from safety requirements
• Verification of safety mechanisms at RTL
• Validation of fault detection and recovery logic
• Evidence generation for safety case documentation This integration ensures that safety verification is not an afterthought, but a structured component of lifecycle assurance.

Limits of Simulation for Safety Sign-off

Simulation remains essential. However, safety-critical designs present structural challenges:

• State-space explosion in complex SoCs
• Rare fault conditions triggered by unusual sequences
• Reset interactions across multiple clock domains
• Subtle protocol corner cases Directed testing can demonstrate behaviour under expected scenarios. It cannot guarantee the absence of unintended behaviour across the entire reachable state space. For higher ASIL targets, confidence must extend beyond sampled behaviour.

Simulation explores selected trajectories through the state space. Formal analysis attempts to prove that no counterexample exists within defined constraints. Where proofs succeed, they provide strong guarantees that certain classes of failure cannot occur.

This distinction becomes particularly relevant for:

• Deadlock freedom
• Safe state transitions
• Correct prioritisation of safety interrupts
• Fault escalation logic

Formal Verification for Safety Proofs

Formal verification for ISO 26262 safety compliance focuses on safety properties such as:

• Correct activation of safety mechanisms
• Guaranteed fault detection within bounded latency
• Proper isolation between safety partitions
• Absence of unintended state machine transitions
• Correct reset and recovery behaviour

Formal methods attempt to prove that these properties hold under all permitted operating conditions. Unlike simulation, which demonstrates the presence of expected behaviour, formal analysis attempts to demonstrate the absence of prohibited behaviour.

This distinction aligns closely with safety objectives, which frequently require proof that hazardous behaviour cannot occur under defined assumptions.

Designs Most Suited to Formal in Safety Contexts

Certain design classes are particularly well-suited to formal analysis in safety-critical environments:

• Control logic and arbitration mechanisms
• Communication protocols and bus interfaces
• Error-handling state machines
• Watchdog and monitoring logic
• Lockstep comparator logic
• Reset sequencing across safety domains

These structures often have finite state representations and well-defined properties, making them amenable to exhaustive reasoning.

Figure 2: Representative automotive SoC safety architecture highlighting formal verification focus areas. Source: Synopsys

Figure 2 illustrates a representative automotive safety processor architecture incorporating lockstep cores, ECC-protected memories, watchdog timers, safety monitors, and secure bus structures. Formal verification is particularly effective for proving the correctness of lockstep comparators, fault-detection logic, reset sequencing, and inter-domain isolation mechanisms in such architectures.

In contrast, datapath-heavy arithmetic blocks may be less suitable for unbounded proofs but can still benefit from targeted formal checks.

Safety Applications in the EDA Ecosystem

Major EDA vendors provide safety-focused formal capabilities integrated into their verification platforms. These solutions typically support:

• Property derivation from safety requirements
• Fault modelling and fault injection analysis
• Proof coverage and completeness metrics
• Traceability support for safety case documentation Examples include formal safety applications within established formal platforms from Synopsys, Cadence, and Siemens. These tools align with ISO 26262 workflows while remaining vendor-neutral in methodology.

The presence of ecosystem support indicates that formal verification has matured into a practical component of automotive safety programmes.

Coverage Closure and Proof-Based Sign-off

Proof alone is not sufficient. Credible safety sign-off requires disciplined closure.

Key elements include:

• Clear definition of safety properties derived from requirements
• Explicit documentation of environmental assumptions
• Identification of bounded versus unbounded proofs
• Vacuity checking to ensure properties are meaningful
• Coverage analysis demonstrating completeness relative to safety goals

Proof coverage metrics and property review processes contribute to an auditable safety argument. Without structured closure criteria, formal verification risks becoming a technical exercise rather than evidence for certification.

These blocks include:

• Safety managers
• Error detection and correction units
• Inter-domain isolation logic
• Redundant comparator structures
• Reset and clock supervision circuits

Applying formal verification at these integration points strengthens the overall safety case.

Automotive SoC Verification Workflow

A structured workflow may proceed as follows:

1. Derive formal properties directly from hardware safety requirements.
2. Model operational modes and fault assumptions explicitly.
3. Apply formal verification to safety-critical control logic.
4. Analyse counterexamples and refine assumptions.
5. Perform coverage and completeness analysis.
6. Document results as part of the safety case evidence.

This approach integrates formal verification into the broader functional safety lifecycle rather than treating it as an isolated activity.

Industrial Adoption Trends

As automotive architectures evolve toward centralised compute and zonal controllers, the complexity of safety mechanisms increases. The verification burden scales accordingly. Formal verification increasingly complements simulation in ASIL-driven programmes. It does not replace established methods but strengthens them by providing evidence-based reasoning when testing alone cannot provide sufficient confidence.

For organisations responsible for silicon sign-off, this additional layer of rigour contributes directly to risk reduction and certification readiness.

Conclusion

ISO 26262 demands objective, traceable evidence that safety requirements are correctly implemented. Simulation remains essential, but it cannot exhaustively explore the full behaviour space of complex automotive SoCs.

Formal verification for ISO 26262 safety compliance provides a structured mechanism to prove critical safety properties, particularly in control logic and safety mechanisms. When integrated into a disciplined workflow with clear assumptions and coverage analysis, formal methods strengthen the overall safety case and increase decision confidence at sign-off.

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/

Further Resources:
👉 https://alpinumconsulting.com/services/training/
👉 https://alpinumconsulting.com/services/

References

[1] ISO 26262-6:2018 Road vehicles – Functional safety – Product development at the hardware level. Available: https://www.iso.org/standard/68388.html

[2] ISO 26262-4:2018 System-level requirements and safety validation. Available: https://files.infocentre.io/files/docs_clients/126_2008096319_4226752_docu_nt_doga_ISO_26262-4.pdf

[3] Clarke, E. et al., Model Checking. MIT Press. Available: https://dl.acm.org/doi/10.5555/778522.778533

[4] Siemens EDA, Functional Safety Verification Methodology Overview. Available: https://www.siemens.com/en-us/products/ic/questa-one/functional-safety/iso-26262/

[5] DVCON Proceedings, A Coverage-Driven Formal Methodology for Verification Sign-off. Available: https://dvcon-proceedings.org/wp-content/uploads/a-coverage-driven-formal-methodology-for-verification-sign-off.pdf