CDC.md

Clock Domain Crossing (CDC)

Clock Domain Crossing (CDC) — Lock-Free Multi-Clock Simulation

Sparkle includes a lock-free CDC infrastructure for Time-Warping simulation across multiple clock domains. Each domain runs on its own thread, connected by a high-performance SPSC queue — no mutexes required.

Architecture

Lean (JIT.runCDC)
  ▼
sparkle_jit.c ──dlopen──▶ cdc_runner.so (C++20)
                              │
                   ┌──────────┴──────────┐
              Thread A (100MHz)    Thread B (50MHz)
              eval_tick + push     pop + set_input + eval_tick
                   └─── SPSC Queue ───┘

Key Features

• Lock-free SPSC queue (c_src/cdc/spsc_queue.hpp): ARM64-optimized, 210M ops/sec, false-sharing prevention
• Rollback mechanism (c_src/cdc/cdc_rollback.hpp): Detects timestamp inversions, restores snapshots — queue indices never rolled back
• 12 formal proofs (Sparkle/Verification/CDCProps.lean): SPSC safety, rollback guarantee, queue index isolation — all proven, no sorry
• JIT integration: JIT.runCDC runs two domains on separate threads from Lean via dlopen bridge

Multi-Clock E2E Test

# Build and run
make -C c_src/cdc           # build cdc_runner.so
lake exe cdc-multi-clock-test
# ╔══════════════════════════════════════════════════╗
# ║   Sparkle CDC Multi-Clock JIT Simulation Test   ║
# ╠══════════════════════════════════════════════════╣
# ║  DomainA: 8-bit counter  (100MHz, 200K cycles)  ║
# ║  DomainB: accumulator    ( 50MHz, 100K cycles)  ║
# ╚══════════════════════════════════════════════════╝
#   Messages sent:     76421
#   Messages received: 75397
#   Rollbacks:         0
# *** CDC Multi-Clock Test: PASS ***

---