Publication
Embedding Modulo Counter Circuits for their Polynomial Formal Verification
Caroline Dominik; Rolf Drechsler
In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV). ITG/GMM/GI-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV-2026), March 11-12, Rostock, Germany, 2025.
Abstract
Proving the correct behavior of hardware by verifying it is a central aspect of maximizing the quality of digital systems.
But this task has a high computational complexity and the required resources of a specific application are usually
unpredictable. This makes the integration into the workflow of modern circuit design challenging. The recent approach of
Polynomial Formal Verification (PFV) aims to identify verification methods and classes of circuits for which an efficient
verification can always be guaranteed - so far with a focus on combinational circuits. A first application to sequential
circuits considered full counter circuits and proposed a method applicable to bijective functions. An efficient verification
could be ensured despite their exponential sequential depth.
Within this paper, this verification approach is extended to be applicable to any modulo counter circuit. For this, bijectivity
of the circuits function is generated by utilizing the concept of embedding. It is theoretically proven that the application
can be carried out in polynomial time and space. Experimental evaluations confirm these theoretical findings