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

被引:1
|
作者
Nadeem, Mohamed [1 ]
Drechsler, Rolf [1 ,2 ]
机构
[1] Univ Bremen, Bremen, Germany
[2] DFKI, Bremen, Germany
关键词
Polynomial Formal Verification; Logic Synthesis; Multi-Valued Logic; Answer Set Programming; Cutwidth;
D O I
10.1109/ISMVL60454.2024.00037
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Formal verification is essential for circuit correctness. Extending binary logic verification to Multi-Valued Logic (MVL) presents challenges due to encoding challenges. Answer Set Programming (ASP) enables compact MVL circuit encoding. In this paper, we propose a Polynomial Formal Verification (PFV) approach for MVL circuits with a constant cutwidth. It employs a divide-and-conquer algorithm to decompose circuits into subcircuits, each representing an output, where ASP is used to encode and verify the subcircuits. The approach reduces verification complexity to the circuit's cutwidth, independent of input bitwidth, ensuring linear time verification for circuits with constant cutwidth. We validate our approach using adder architectures, as many adder architectures have a constant cutwidth. Empirical experiments involve various adder architectures and different logic levels.
引用
收藏
页码:149 / 154
页数:6
相关论文
共 50 条
  • [1] Polynomial Formal Verification of Multi-Valued Approximate Circuits Within Constant Cutwidth
    Nadeem, Mohamed
    Jha, Chandan Kumar
    Drechsler, Rolf
    IEEE TRANSACTIONS ON CIRCUITS AND SYSTEMS I-REGULAR PAPERS, 2025,
  • [2] Polynomial Formal Verification exploiting Constant Cutwidth
    Nadeem, Mohamed
    Kleinekathoefer, Jan
    Drechsler, Rolf
    PROCEEDINGS OF THE 2023 34TH INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, RSP 2023, 2023,
  • [3] Polynomial Formal Verification of Approximate Adders with Constant Cutwidth
    Nadeem, Mohamed
    Jha, Chandan Kumar
    Drechsler, Rolf
    IEEE EUROPEAN TEST SYMPOSIUM, ETS 2024, 2024,
  • [4] Verification of multi-valued logic networks
    Drechsler, R
    1996 26TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 1996, : 10 - 15
  • [5] Polynomial-Time Formal Verification of Adder Circuits for Multiple-Valued Logic
    Niemann, Philipp
    Drechslee, Rolf
    2022 IEEE 52ND INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC (ISMVL 2022), 2022, : 9 - 14
  • [6] Basic circuits for multi-valued sequential logic
    Fatma Sarica
    Avni Morgül
    Analog Integrated Circuits and Signal Processing, 2013, 74 : 91 - 96
  • [7] Basic circuits for multi-valued sequential logic
    Sarica, Fatma
    Morgul, Avni
    ANALOG INTEGRATED CIRCUITS AND SIGNAL PROCESSING, 2013, 74 (01) : 91 - 96
  • [8] Magnonic interferometric switch for multi-valued logic circuits
    Balynsky, Michael
    Kozhevnikov, Alexander
    Khivintsev, Yuri
    Bhowmick, Tonmoy
    Gutierrez, David
    Chiang, Howard
    Dudko, Galina
    Filimonov, Yuri
    Liu, Guanxiong
    Jiang, Chenglong
    Balandin, Alexander A.
    Lake, Roger
    Khitun, Alexander
    JOURNAL OF APPLIED PHYSICS, 2017, 121 (02)
  • [9] MULTI-VALUED LOGIC
    PERRINE, S
    ANNALES DES TELECOMMUNICATIONS-ANNALS OF TELECOMMUNICATIONS, 1978, 33 (11-1): : 376 - 382
  • [10] Fault characterization and testability considerations in Multi-Valued logic circuits
    Abd-El-Barr, M
    Al-Sherif, M
    Osman, M
    1999 29TH IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 1999, : 262 - 267