Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines

Abstract

Tapped delay lines (TDLs) implemented in field-programmable gate array (FPGA) carry-chain primitives are central to high-resolution time-to-digital converters (TDCs). However, TDLs are prone to bubble errors, i.e., local thermometer-code violations caused by implementation-dependent delay inversions and metastability, which are still treated largely by empirical post-silicon filtering rather than by design-time proof. We present an ordering-relation abstraction for formal verification of bubble behaviour in an explicit abstract threshold model. The abstraction replaces continuous delay magnitudes with a finite Boolean domain over adjacent tap orderings, thereby enabling exhaustive symbolic analysis of ordering-dependent safety properties. The method is instantiated on a reference 8-tap CARRY8-based TDL and verified in three phases: binary decision diagram (BDD)-based model checking in NuSMV, cross-solver validation in nuXmv, and IC3/PDR-based scaling to larger TDL chains. The verification establishes five structural results in the model: local bubble-inversion causality, mutual exclusion of simultaneous raw bubbles, monotonicity of three-tap majority suppression, structural survival of boundary bubbles under suppression, and reachability of recovery from sampled-bubble states. These results provide assumption-qualified design-time checks and decoder/filtering guidance that complement simulation and post-silicon characterisation.