Abstract | ||
---|---|---|
Division is one of the most complex and hard to verify arithmetic operations. While verification of major arithmetic operators, such as adders and multipliers, has significantly progressed in recent years, less attention has been devoted to formal verification of dividers. A type of divider that is often used in embedded systems is divide by a constant. This paper presents a formal verification method for different divide-by-constant architectures and the generic restoring dividers based on the computer algebra approach. Our experiments for different divider architectures and comparison with exhaustive simulation demonstrates the effectiveness and scalability of the method. |
Year | DOI | Venue |
---|---|---|
2019 | 10.1109/ISVLSI.2019.00022 | 2019 IEEE Computer Society Annual Symposium on VLSI (ISVLSI) |
Keywords | Field | DocType |
Constant Divider,Formal Verification,LUT,Restoring Divider,Algebraic Rewriting,Vanishing Monomials,Simulation | Integer,Logic gate,Adder,Computer science,Symbolic computation,Arithmetic,Arithmetic operators,Formal verification,Scalability | Conference |
ISSN | ISBN | Citations |
2159-3469 | 978-1-7281-3392-8 | 1 |
PageRank | References | Authors |
0.37 | 10 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Atif Yasin | 1 | 6 | 1.86 |
Tiankai Su | 2 | 6 | 2.19 |
Sébastien Pillement | 3 | 1 | 0.37 |
Maciej J. Ciesielski | 4 | 629 | 74.80 |