Clock Domain Crossing (Clock Domain Crossing (CDC)) verification plays a crucial role in modern digital system design to ensure accurate and reliable data transfer between asynchronous clock domains. This paper investigates two prevalent verification methods—simulation-based verification and formal verification—highlighting their respective strengths and limitations in the context of CDC. Simulation-based verification, commonly implemented through the Universal Verification Methodology (UVM), is widely adopted for its adaptability in handling complex designs. By utilizing randomized stimuli, testbench automation, and reference modules, it provides an efficient environment for functional coverage. However, it often encounters challenges such as incomplete coverage, long simulation cycles, and the inability to uncover corner-case scenarios. On the other hand, formal verification relies on mathematical modeling and exhaustive exploration of all possible circuit states, enabling a more thorough verification process. Using tools like the JasperGold CDC app, it ensures functional correctness by validating circuit behavior against predefined rules and assertions. Despite its exhaustive nature, formal verification faces significant limitations, including scalability issues, state explosion, and reliance on computational resources. This study analyzes a simulation-based CDC metastability injection model and compares it with formal verification methods to identify gaps and opportunities for improvement. The results demonstrate the complementary strengths of these approaches, suggesting that an integrated verification strategy may be the most effective for future CDC designs. This research provides valuable insights for practitioners aiming to enhance the reliability and efficiency of CDC verification workflows.

Clock Domain Crossing (CDC)-verifiering spelar en avgörande roll i modern digital systemdesign för att säkerställa korrekt och tillförlitlig dataöverföring mellan asynkrona klockdomäner. Denna artikel undersöker två vanliga verifieringsmetoder—simuleringsbaserad verifiering och formell verifiering—och belyser deras respektive styrkor och begränsningar i CDC- sammanhang. Simuleringsbaserad verifiering, som ofta implementeras genom Universal Verification Methodology (UVM), är allmänt använd för sin anpassningsför- måga vid hantering av komplexa designer. Genom att använda slumpmässiga stimuli, automatisering av testbänkar och referensmoduler skapar den en effektiv miljö för funktionell täckning. Dock möter den ofta utmaningar såsom ofullständig täckning, långa simuleringscykler och oförmåga att identifiera hörnfallsscenarier. Formell verifiering, å andra sidan, bygger på matematisk modellering och uttömmande utforskning av alla möjliga tillstånd i en krets, vilket möjliggör en mer grundlig verifieringsprocess. Med verktyg som JasperGold CDC- app säkerställs funktionell korrekthet genom att validera kretsbeteenden mot fördefinierade regler och påståenden. Trots sin omfattande natur står formell verifiering inför betydande begränsningar, inklusive skalbarhetsproblem, tillståndsexplosion och beroende av beräkningsresurser. Denna studie analyserar en simuleringsbaserad modell för CDC-metastabilitet och jämför den med formella verifieringsmetoder för att identifiera luckor och förbättringsmöjligheter. Resultaten visar på de kompletterande styrkorna hos dessa tillvägagångssätt och föreslår att en integrerad verifieringsstrategi kan vara den mest effektiva för framtida CDC-design. Forskningen ger värdefulla insikter för praktiker som strävar efter att förbättra tillförlitligheten och effektiviteten i CDC-verifieringsarbetsflöden.