Computer Algebraic Approach to Verification and Debugging of Galois Field Multipliers

被引：0
|
作者：
Su, Tiankai [1 ]
Yasin, Atif [1 ]
Yu, Cunxi [1 ,2 ]
Ciesielski, Maciej [1 ]
机构：
[1] Univ Massachusetts, ECE Dept, Amherst, MA 01003 USA
[2] Ecole Polytech Fed Lausanne, LSI, Lausanne, Switzerland
来源：
2018 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS (ISCAS) | 2018年
基金：
美国国家科学基金会;
关键词：
Galois Field; Arithmetic circuits; Formal verification; Computer Algebra; Logic Debugging;
D O I：
10.1109/ISCAS.2018.8351397
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
The paper presents a novel method to verify and debug gate-level arithmetic circuits implemented in Galois Field arithmetic. The method is based on forward reduction of the specification polynomials of the circuit in GF(2(m)) using GF(2) models of its logic gates. We define a forward variable order "FO >" and the rules of forward reduction that enable verification, bug detection, and automatic bug correction in the circuit. By analyzing the remainder generated by forward reduction, the method can determine whether the circuit is buggy, and finds the location and the type of the bug. The experiments performed on Mastrovito and Montgomery multipliers show that our debugging method is independent of the location of the bug(s) and the debugging time is comparable to the time needed to verify the bug-free circuit.
引用
收藏
页数：5
相关论文
共 50 条
  • [1] Efficient Parallel Verification of Galois Field Multipliers
    Yu, Cunxi
    Ciesielski, Maciej
    2017 22ND ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC), 2017, : 238 - 243
  • [2] EFFICIENT GROBNER BASIS REDUCTIONS FOR FORMAL VERIFICATION OF GALOIS FIELD MULTIPLIERS
    Lv, Jinpeng
    Kalla, Priyank
    Enescu, Florian
    DESIGN, AUTOMATION & TEST IN EUROPE (DATE 2012), 2012, : 899 - 904
  • [3] VERIFICATION OF COMPOSITE GALOIS FIELD MULTIPLIERS OVER GF((2m)n) USING COMPUTER ALGEBRA TECHNIQUES
    Lv, Jinpeng
    Kalla, Priyank
    Enescu, Florian
    2011 IEEE INTERNATIONAL HIGH LEVEL DESIGN VALIDATION AND TEST WORKSHOP (HLDVT), 2011, : 136 - 143
  • [4] FORMAL VERIFICATION OF SEQUENTIAL GALOIS FIELD ARITHMETIC CIRCUITS USING ALGEBRAIC GEOMETRY
    Sun, Xiaojun
    Kalla, Priyank
    Pruss, Tim
    Enescu, Florian
    2015 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2015, : 1623 - 1628
  • [5] Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
    Lvov, Alexey
    Lastras-Montano, Luis A.
    Trager, Barry
    Paruthi, Viresh
    Shadowen, Robert
    El-Zein, Ali
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 45 (02) : 189 - 212
  • [6] Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
    Alexey Lvov
    Luis A. Lastras-Montaño
    Barry Trager
    Viresh Paruthi
    Robert Shadowen
    Ali El-Zein
    Formal Methods in System Design, 2014, 45 : 189 - 212
  • [7] Flexible VLSI architectures for Galois field multipliers
    Basiri, Mohamed Asan M.
    Shukla, Sandeep K.
    INTEGRATION-THE VLSI JOURNAL, 2017, 59 : 109 - 124
  • [8] On the design of reconfigurable multipliers for integer and Galois field multiplication
    Hinkelmann, Heiko
    Zipf, Peter
    Li, Jia
    Liu, Guifang
    Glesner, Manfred
    MICROPROCESSORS AND MICROSYSTEMS, 2009, 33 (01) : 2 - 12
  • [9] Hierarchical verification of Galois field circuits
    Mukhopadhyay, Debdeep
    Sengar, Gaurav
    Chowdhury, Dipanwita Roy
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2007, 26 (10) : 1893 - 1898
  • [10] Formal Verification of Constrained Arithmetic Circuits using Computer Algebraic Approach
    Su, Tiankai
    Yasin, Atif
    Pillement, Sebastien
    Ciesielski, Maciej
    2020 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI (ISVLSI 2020), 2020, : 386 - 391
12345