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

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.