Provably Correct and Scalable Clock Modeling for FPGA-based Emulation

Field-programmable gate array (FPGA)-based emulation delivers orders of magnitude higher throughput than software simulation. However, fundamental clocking differences between application-specific integrated circuits (ASICs) and FPGAs limit its performance and capacity. To address this, we model the sampling of all flip-flops (FFs), originally triggered by multiple generated clocks, as an ordered sequence of events and reproduce their behavior at each emulation step. We introduce two clock models. The output-gated model (M _o ) samples the clock, input, and output of each FF, requiring more logic resources but no event ordering. Conversely, the sampling-gated model (M _s ) uses clock edge detection to conditionally sample, using fewer logic resources but requiring event ordering. We then adopt a hybrid strategy that applies M _o to clock-generation logic to avoid resolving complex clock dependencies, and applies M _s to the data path to save logic resources. We formally prove that the transformed design is sequentially equivalent to the original at every emulation step. We propose matching-point inductive verification (MPIV), which augments the inductive proof with matching points recorded during the transformation and reduces verification tasks to satisfiability (SAT) checks. Across industrial designs with up to 11,515 generated clocks, the hybrid approach incurs modest overhead (1.7% FFs and 5.8% lookup tables (LUTs) on average). MPIV achieves up to 2,950 × speedup and succeeds on large designs where a widely used model checker ABC-PDR times out. To the best of our knowledge, this is the first publicly documented and formally verified methodology for eliminating logic-generated clocks in ASIC-to-FPGA emulation.