Name
Abstract | ||
|---|---|---|
The paper describes a method of verifying sequential arithmetic circuits by adding a special type of redundancy, called “Vanishing Polynomials” and “Don't Care Polynomials”. The proof of functional correctness consists in transforming the polynomial expression at the primary outputs into a unique polynomial in the primary inputs and comparing the computed expression against the expected specification. Experimental results show that the technique is efficient and scalable; for example, a 512-bit serial squarer requiring over 2000 clock cycles was verified in just 330 seconds. The runtime complexity is linear and memory complexity is quadratic in the number of gates. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/ISVLSI.2016.59 | 2016 IEEE Computer Society Annual Symposium on VLSI (ISVLSI) |
Keywords | Field | DocType |
formal verification,computer algebraic,sequential arithmetic circuits | PH,Boolean circuit,Polynomial,Computer science,Arithmetic,Theoretical computer science,Descriptive complexity theory,Arithmetic circuit complexity,High-level verification,Formal verification | Conference |
ISSN | ISBN | Citations |
2159-3469 | 978-1-4673-9040-8 | 0 |
PageRank | References | Authors |
0.34 | 14 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cunxi Yu | 1 | 98 | 9.64 |
| Maciej J. Ciesielski | 2 | 629 | 74.80 |