Name
Title | ||
|---|---|---|
Formal Verification of Truncated Multipliers Using Algebraic Approach and Re-Synthesis |
Abstract | ||
|---|---|---|
This paper presents a formal approach to verify multipliers that approximate integer multiplication by output truncation. The method is based on extracting polynomial signature of a truncated multiplier using algebraic rewriting. To efficiently compute the polynomial signature, a multiplier reconstruction approach is used to construct the precise multi- plier from the truncated one. The method consists of three basic steps: 1) determine the weights (binary encoding) of the output bits; 2) reconstruct the truncated multiplier using functional merging and re-synthesis; and 3) construct the polynomial signature of the resulting circuit. The method has been tested on multipliers up to 256 bits with three truncation schemes: Deletion, D-truncation, and Truncation with Rounding. Experimental results are compared with the state-of-the-art SAT, SMT, and computer algebraic solvers. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ISVLSI.2017.79 | 2017 IEEE Computer Society Annual Symposium on VLSI (ISVLSI) |
Keywords | Field | DocType |
Formal Verification,Truncated Multipliers,Approximate Computing,Computer Algebra. | Truncation,Algebraic number,Adder,Polynomial,Computer science,Algorithm,Multiplier (economics),Rounding,Rewriting,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-5090-6763-3 | 1 | 0.37 |
References | Authors | |
12 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tiankai Su | 1 | 1 | 0.37 |
| Cunxi Yu | 2 | 98 | 9.64 |
| Atif Yasin | 3 | 1 | 1.72 |
| Maciej J. Ciesielski | 4 | 629 | 74.80 |