Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures.
Saved in:
| Title: | Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures. |
|---|---|
| Authors: | NADEEM, MOHAMED1 mnadeem@uni-bremen.de, DRECHSLER, ROLF1,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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 194269964 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22NADEEM%2C+MOHAMED%22">NADEEM, MOHAMED</searchLink><relatesTo>1</relatesTo><i> mnadeem@uni-bremen.de</i><br /><searchLink fieldCode="AR" term="%22DRECHSLER%2C+ROLF%22">DRECHSLER, ROLF</searchLink><relatesTo>1,2</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Multiple-Valued+Logic+%26+Soft+Computing%22">Journal of Multiple-Valued Logic & Soft Computing</searchLink>. 2026, Vol. 47 Issue 1, p103-130. 28p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Formal+verification%22">Formal verification</searchLink><br /><searchLink fieldCode="DE" term="%22Many-valued+logic%22">Many-valued logic</searchLink><br /><searchLink fieldCode="DE" term="%22Circuit+complexity%22">Circuit complexity</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+design%22">Logic design</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+circuits%22">Logic circuits</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=194269964 |
| RecordInfo | BibRecord: BibEntity: Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 28 StartPage: 103 Subjects: – SubjectFull: Formal verification Type: general – SubjectFull: Many-valued logic Type: general – SubjectFull: Circuit complexity Type: general – SubjectFull: Logic design Type: general – SubjectFull: Logic circuits Type: general Titles: – TitleFull: Linear Formal Verification of Multi-Valued Logic Circuits within Constant Cutwidth Architectures. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: NADEEM, MOHAMED – PersonEntity: Name: NameFull: DRECHSLER, ROLF IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 01 Text: 2026 Type: published Y: 2026 Identifiers: – Type: issn-print Value: 15423980 Numbering: – Type: volume Value: 47 – Type: issue Value: 1 Titles: – TitleFull: Journal of Multiple-Valued Logic & Soft Computing Type: main |
| ResultId | 1 |
