SHF: Small: Word-level Abstraction of Arithmetic Gate-level Circuits

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

With an ever-increasing complexity of integrated circuits, hardware verification has become the dominating factor of the overall electronic design flow. Particularly critical and challenging is the verification of complex arithmetic components present in almost every design, from microprocessors to medical devices to a communication equipment. In contrast to logic circuits, for which effective Boolean methods have been developed, the difficulty of arithmetic hardware verification lies in the size and the amount of data that needs to be analyzed. Different mathematical models, based on higher abstraction level than logic bits need to be developed to deal with this complexity. This project addresses this problem by developing new techniques for abstracting arithmetic structures from physical circuit implementations. In addition to verification, abstracting higher-level information from a design is important in hardware trust and security applications, where it can be used to analyze the design to isolate malicious hardware. Successful implementation of this work will contribute to the development of the state-of-the-art tools for electronic design automation and will increase design productivity. The project will also train undergraduate and graduate students, postdocs for future workforce in this technical area. The project will develop a new method to abstract high-level information from arithmetic circuits using computer algebra approach. In this approach, circuit components, such as logic gates, are modeled in algebraic domain as pseudo-Boolean polynomials. Rewriting polynomials from circuit outputs to inputs makes it possible to extract arithmetic function embedded in the circuit. During the rewriting, the intermediate pseudo-Boolean expressions are examined in order to identify possible arithmetic structures. The identification is done using a novel "spectral analysis" technique, which matches the polynomial expressions against the reference "spectra" of basic arithmetic blocks, such as multipliers, adders, and multiply-and-accumulate operators. This approach will abstract word components from polynomial expressions to reason about the word-level structure from the internal expressions. By representing logic and arithmetic functions as pseudo-Boolean polynomials, it is possible to mitigate the size explosion typically encountered in Boolean based methods.