Immutable Truths as Simulation Drivers An AI-Powered Workflow for Translating Architectural Formal Specifications into C-Based Simulation Components

Modern System-on-Chip (SoC) complexity necessitates rigorous pre-RTL architectural formal verification to eliminate critical bugs early, as flaws discovered late in the design cycle are orders of magnitude more costly to fix, triggering expensive RTL rewrites or silicon respins. In this flow, architectural formal verification engineers construct high-level behavioral models using the Murphi description language and use the Murphi model checker to exhaustively verify architecture specifications for functional completeness, deadlock-freedom, and safety property compliance. However, a persistent verification gap exists between these declarative formal specifications and the procedural C-models required for high-performance architectural simulation and subsequent Register Transfer Level (RTL) validation. Traditionally, this translation is performed manually, introducing "Specification Drift" and risking the re-introduction of the very bugs formal verification aimed to eliminate. This paper proposes a 3-Pillar methodology leveraging Generative AI (Gemini) to automate the semantic synthesis of executable C-models directly from verified Murphi specifications. By treating the Murphi formal model as the Single Root of Truth (SRoT), we ensure protocol invariants are inherited with zero divergence. Implementation on an internal Connectivity IP (CIP) demonstrates an 85% reduction in C-model development time, moving from a 6-week manual effort to a 3-day automated flow, while achieving 100% functional parity.