Suggested Reading for ECE 667

This is an OLD material - should be updated soon ...

These are some of the papers to choose from for your research and class presentation. More papers are available by personal request.

M. Ciesielski, P. Kalla, etc., "LPSAT: A Unified Approach to RTL Satisfiability" (PS file). - functional test generation using linear integer programming.

"Verification of Arithmetic Circuits by Computing Algebraic Signature" - a linear algebra approach to prove functional correctness of arithmetic circuits, such as adders and multipliers.
Ask Basith for a hard copy of the paper we recently submitted to DAC'2011 conference. Since this is an unpublished paper, I can only distribute a hard copy.

For more, you should search the literature (Google to the rescue ...) for topics, such as:

Functional decomposition (Asenhurst-Kurtis type);
Power estimiation on logic level by computing switching activity;
Model checking, property checking;
Equivalence checking;
ABL (arithmetic boolean level) verification;
Binary matching (in standard cell technology mapping);
Some kind of tutorial on SMT (satisfiability modulo theories), which combines Boolean, integer, arithmetic operations.

High Level Synthesis

D. Chen, J. Cong, et al., "LOPASS: A Low Power Architectural Synthesis System for FPGAs with Interconnect Estimation and Optimization".
A low power architectural synthesis system which addresses power issue by minimizing stearing logic (MUXes, wiring, etc.)

J. Cong, et. al., "High-Level Synthesis for FPGAs: From Prototyping to Deployment"
A thorough survey of high-level synthesis methods.

Logic Synthesis

C. Yang, M. Ciesielski, "BDS - A BDD-based Logic Optimization System", IEEE Trans. on CAD, July 2002.
BDD-based synthesis system; addresses Boolean level logic optimization by BDD decomposition.

A. Mishchenko et. al ABC basics .

A. Mishchenko, S. Chatterjee, R. Brayton, "Scalable Logic Synthesis using a Simple Circuit Structure".
Basic paper on ABC synthesis system, a de-facto standard logic synthesis today, worth reading and understanding! Uses AIG data structure to manipulate logic.

A. Mishchenko, et. al., "DAG-Aware AIG Rewriting: A Fresh Look at Combinational Logic Synthesis", DAC 2006, Another paper on ABC, describes rewriting of And-Inverter Graphs (AIG) as a basic method for heuristic logic optimization.

A. Mishchenko, et. al., "Integrating Logic Synthesis, Technology Mapping, and Retiming"
Integrating all phases of logic synthesis together. A very ambitious work !

D. Chen, J. Cong, "DAOmap: A Depth-optimal Area Optimization Mapping Algorithm for FPGA Designs", ICCAD'04.
Studies technology mapping problem for FPGA architectures to minimize chip area, measured as the total number of lookup tables (LUTs) of the mapped design, under the chip performance constraint.

Binary (and other) Decision Diagrams

R. Bryant, Y. Chen, "Verification of Arithmetic Circuits using Binary Moment Diagrams".
Original paper on (BMD (Binary Moment Diagrams), a more abstract represeentation than BDDs, from the inventor of BDDs.

Y. Chen, J. Cong, "PHDD: An Efficient Graph Representation for Floating Point Circuit Verification"
BMDs used for floating point arithmetic verification.

M. Ciesielski, P. Kalla, S. Askar, "Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs", TCOMP 2006.
Original paper on TEDs, a higher level abstract representation for data flow designs.

M. Ciesielski et. al., "Optimization of Data Flow Computations using Canonical TED Representation", TCAD, Sept. 2009.
Application of TEDs to high-level synthesis; finding best DFG representation.

R. Anderson, An Introduction to Binary Decision Diagrams, (37 pages), 1997. A concise tutorial on BDDs.

F. Somenzi, Binary Decision Diagrams, (67 pages), 1998. A complete document on BDDs, including: BDD theory, diagram manipulation, variable ordering, implementation issues, image computation, and more. By the author of the famous CUDD package.

Satisfiability (SAT)

J.P. Marques-Silva, K. Sakallah, "Boolean Satisfiability in Electronic Design Automation", DAC 2000. Review of stisfiability (SAT) problem.

Binate Covering Problem

O. Coudert, "On Solving Covering Problems".
This paper describes heuristics for solving the binate covering problem (BCP), useful in technology mapping.

Formal Verification

S. Vasudevan, ... ,J. Abraham, et.al, "Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems" TCOMP, Oct. 2007. Presents technique for proving correctness of arithmetic circuit designs described at the Register Transfer Level (RTL), based on term rewriting.

C.A.J. Van Eijk, "Sequential Equivalence Checking Based on Structural Similarities", TCAD 2000.
Seminal paper on sequential verification (equivalence checking) using inductive method.

A. Kuehlman, F. Krohm, "Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification".
Combination of techniques for Boolean reasoning based on BDDs, structural transformations, SAT procedure, and random simulation working on a shared graph representation (AIG) of the problem. One of the first uses of AIG in synthesis and equivalence checking.