Finite State Machine Model Checking of a Wave-Union-Based TDC FPGA System
2024 IEEE Workshop on Microwave Theory and Technology in Wireless Communications (MTTW 2024): Proceedings 2024
Jakovs Ratners, Nikolajs Tihomorskis, Sandis Migla, Artūrs Āboltiņš

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.


Atslēgas vārdi
wave-union, time measurement, converters, formal verification, field programmable gate arrays, model checking
DOI
10.1109/MTTW64344.2024.10742184
Hipersaite
https://ieeexplore.ieee.org/document/10742184

Ratners, J., Tihomorskis, N., Migla, S., Āboltiņš, A. Finite State Machine Model Checking of a Wave-Union-Based TDC FPGA System. No: 2024 IEEE Workshop on Microwave Theory and Technology in Wireless Communications (MTTW 2024): Proceedings, Latvija, Riga, 2.-4. oktobris, 2024. Piscataway: IEEE, 2024, 18.-23.lpp. ISBN 979-8-3315-3318-2. e-ISBN 979-8-3315-3317-5. Pieejams: doi:10.1109/MTTW64344.2024.10742184

Publikācijas valoda
English (en)
RTU Zinātniskā bibliotēka.
E-pasts: uzzinas@rtu.lv; Tālr: +371 28399196