Automatic word-level abstraction of datapath
Cunxi Yu, Maciej J. Ciesielski · 2016
Abstracting word information from gate-level designs is essential for formal verification, technology mapping and hardware security applications. In this paper, we present a novel method to abstract the word-level information from arithmetic gate-level circuits using a computer algebraic approach. The proposed technique translates the gate-level circuit into algebraic domain and applies algebraic rewriting to extract the arithmetic function. During the iterative rewriting, intermediate Pseudo-Boolean expressions are examined to identify word-level candidates. The proposed algorithm is able to abstract the word components from candidates and to reason about the word operation from the internal expressions. Successful experiments were performed on gate-level datapaths, including multipliers of up to 128-bit widths.