Name
Abstract | ||
|---|---|---|
The paper describes an algebraic approach to functional verification of arithmetic circuits specified at bit level. The circuit is represented as a network of half adders, full adders, and inverters, and modeled as a system of linear equations. The proof of functional correctness of the design is obtained by computing its algebraic signature using standard LP solver and comparing it with the reference signature provided by the designer. Initial experimental results and comparison with SMT solvers show that the method is efficient, scalable and applicable to large arithmetic designs, such as multipliers. |
Year | Venue | Keywords |
|---|---|---|
2011 | FMCAD | arithmetic circuit,arithmetic design verification,functional correctness,bit level,smt solvers show,large arithmetic design,algebraic approach,reference signature,algebraic signature,full adder,functional verification,vectors,equational logic,equivalence checking,logic gates,linear equations,mathematical model,formal verification,logic design,radiation detector,integrated circuit,adders,radiation detectors |
Field | DocType | Citations |
Formal equivalence checking,Logic synthesis,Functional verification,Adder,Computer science,Correctness,Algorithm,Arithmetic,Theoretical computer science,Solver,Algebraic operation,Formal verification | Conference | 4 |
PageRank | References | Authors |
0.48 | 7 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mohamed Abdul Basith | 1 | 4 | 0.48 |
| Tariq Ahmad | 2 | 6 | 1.54 |
| André Rossi | 3 | 4 | 0.48 |
| Maciej J. Ciesielski | 4 | 629 | 74.80 |