Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures.

Saved in:

Bibliographic Details
Title:	Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures.
Authors:	NADEEM, MOHAMED¹ mnadeem@uni-bremen.de, DRECHSLER, ROLF^1,2
Source:	Journal of Multiple-Valued Logic & Soft Computing. 2026, Vol. 47 Issue 1, p103-130. 28p.
Subjects:	Formal verification, Many-valued logic, Circuit complexity, Logic design, Logic circuits
Abstract:	Formal verification is an essential task to ensure the functional correctness of circuits. While several formal verification methods exist to ensure the functional correctness of circuits, they do not provide tight upper bounds for space and time complexities. Therefore, Polynomial Formal Verification (PFV) has been introduced to tackle this problem. In prior work, it has been shown that binary circuits with constant cutwidth can be verified in linear time using Answer Set Programming (ASP). Extending binary logic verification to Multi-Valued Logic (MVL) presents challenges due to the computational complexity of MVL gates and their encodings. In this paper, we propose Linear Formal Verification (LFV) of MVL circuits as a subclass of PFV. Additionally, we prove that MVL circuits with constant cutwidth can be verified in linear time and space. Finally, we evaluate circuits with constant cutwidth in terms of the upper bound of the cutwidth and verification time under different logic levels to confirm our theoretical findings. [ABSTRACT FROM AUTHOR]
	Copyright of Journal of Multiple-Valued Logic & Soft Computing is the property of Old City Publishing, Inc. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	Formal verification is an essential task to ensure the functional correctness of circuits. While several formal verification methods exist to ensure the functional correctness of circuits, they do not provide tight upper bounds for space and time complexities. Therefore, Polynomial Formal Verification (PFV) has been introduced to tackle this problem. In prior work, it has been shown that binary circuits with constant cutwidth can be verified in linear time using Answer Set Programming (ASP). Extending binary logic verification to Multi-Valued Logic (MVL) presents challenges due to the computational complexity of MVL gates and their encodings. In this paper, we propose Linear Formal Verification (LFV) of MVL circuits as a subclass of PFV. Additionally, we prove that MVL circuits with constant cutwidth can be verified in linear time and space. Finally, we evaluate circuits with constant cutwidth in terms of the upper bound of the cutwidth and verification time under different logic levels to confirm our theoretical findings. [ABSTRACT FROM AUTHOR]
ISSN:	15423980