Finite state machine model checking of a wave-union-based TDC FPGA system

This paper introduces the initial steps towards formal verification of a wave-union based time-to-digital converter (TDC) system designed in a field-programmable gate array (FPGA). Although a wave-union-based TDCs has demonstrated high single-shot precision (tens of picoseconds and even smaller), low dead time, and scalable reconfigurability, it presents significant implementation and calibration challenges due to its strong dependence on the low-level FPGA architecture and its parameters. This paper proposes model checking as the key initial method to verify the correctness of the wave-union-based system. Two finite state machiness (FSMs) were constructed: a reference FSM describing the operation in terms of hardware signals, and a more abstract implementation FSM based on logic assertions derived from the reference FSM. The state transitions were defined using linear temporal logic (LTL). The implementation FSM was analyzed in NuSMV model checker for deadlock-free operation. The result revealed loopback errors which may lead to potential deadlocks. Overall, the verification process demonstrated that the implementation FSM very effectively simulates the operation of a wave-union-based TDC system and can be used for more complex formal verification procedures, such as reachability analysis. This work lays the foundation for research into the formal verification of a wave-union TDC implemented in FPGA.