Word-level abstraction from combinational circuits using algebraic geometry

Update Item Information
Publication Type dissertation
School or College College of Engineering
Department Electrical & Computer Engineering
Author Pruss, Tim
Title Word-level abstraction from combinational circuits using algebraic geometry
Date 2015-08
Description Abstraction plays an important role in digital design, analysis, and verification, as it allows for the refinement of functions through different levels of conceptualization. This dissertation introduces a new method to compute a symbolic, canonical, word-level abstraction of the function implemented by a combinational logic circuit. This abstraction provides a representation of the function as a polynomial Z = F(A) over the Galois field F2k , expressed over the k-bit input to the circuit, A. This representation is easily utilized for formal verification (equivalence checking) of combinational circuits. The approach to abstraction is based upon concepts from commutative algebra and algebraic geometry, notably the Grobner basis theory. It is shown that the polynomial F(A) can be derived by computing a Grobner basis of the polynomials corresponding to the circuit, using a specific elimination term order based on the circuits topology. However, computing Grobner bases using elimination term orders is infeasible for large circuits. To overcome these limitations, this work introduces an efficient symbolic computation to derive the word-level polynomial. The presented algorithms exploit i) the structure of the circuit, ii) the properties of Grobner bases, iii) characteristics of Galois fields F2k , and iv) modern algorithms from symbolic computation. A custom abstraction tool is designed to efficiently implement the abstraction procedure. While the concept is applicable to any arbitrary combinational logic circuit, it is particularly powerful in verification and equivalence checking of hierarchical, custom designed and structurally dissimilar Galois field arithmetic circuits. In most applications, the field size and the datapath size k in the circuits is very large, up to 1024 bits. The proposed abstraction procedure can exploit the hierarchy of the given Galois field arithmetic circuits. Our experiments show that, using this approach, our tool can abstract and verify Galois field arithmetic circuits up to 1024 bits in size. Contemporary techniques fail to verify these types of circuits beyond 163 bits and cannot abstract a canonical representation beyond 32 bits.
Type Text
Publisher University of Utah
Subject Abstraction; Digital Design; Formal Verification; Grobner Basis; Hardware Verification
Dissertation Institution University of Utah
Dissertation Name Doctor of Philosophy
Language eng
Rights Management Copyright © Tim Pruss 2015
Format Medium application/pdf
Format Extent 27,335 bytes
Identifier etd3/id/3965
ARK ark:/87278/s6sf64j7
Setname ir_etd
ID 197515
Reference URL https://collections.lib.utah.edu/ark:/87278/s6sf64j7