Fall 2011

• News

  EE Times - Kaufman award honors Brayton

  SCD source newsletter - Logic synthesis pioneer eyes new horizons

  
  

• Boolean Algebra

  F. Brown. Boolean Reasoning: The Logic of Boolean Equations. Dover Publications, 2003. (Reserved in NTU main library)

  
  

• BDD

  R. E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.

  S. Minato. Zero-Supressed BDD's for Set Manipulation in Combinatorial Problems. In Proc. Design Automation Conference, 1993.

  A. Mishchenko. An Introduction to Zero-Supressed Binary Decision Diagrams. Technical report, Portland State University, June 2001.

  
  

• SAT

  J. Marques-Silva and K. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability.  IEEE Transactions on Computers, vol. 48, no. 5, May 1999.

  M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proc. Design Automation Conference, 2001.

  N. Eén and N. Sörensson. An Extensible SAT-solver. In Proc. SAT, 2003.

  S. Malik's talk on The Quest for Efficient Boolean Satisfiability Solvers, 2004.

  M. Sheeran and Gunnar Stålmarck. A Tutorial on Stålmarcks's Proof Procedure for Propositional Logic. In Proc. Formal Methods in Computer Aided Ddesign 1998.

  
  

• Interpolation-based Logic Synthesis

  Chih-Chun Lee, Jie-Hong R. Jiang, Chung-Yang (Ric) Huang, and Alan Mishchenko. Scalable Exploration of Functional Dependency by Interpolation and Incremental SAT Solving. In Proc. ICCAD, 2007.

  Ruei-Rung Lee, Jie-Hong R. Jiang, and Wei-Lun Hung. Bi-Decomposing Large Boolean Functions via Interpolation and Satisfiability Solving. In Proc. DAC, 2008.

  Hsuan-Po Lin, Jie-Hong R. Jiang, and Ruei-Rung Lee. To SAT or Not to SAT: Ashenhurst Decomposition in a Large Scale. In Proc. ICCAD, 2008.

  Alan Mishchenko, Robert K. Brayton, Jie-Hong R. Jiang, and Stephen Jang. Scalable don't care based logic optimization and resynthesis. In Proc. FPGA, 2009.

  
  

• Recursive Learning

  W. Kunz and D. Pradhan. Recursive Learning: A New Implication Technique for Efficient Solutions to CAD Problems - Test, Verification, and Optimization. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, issue 9, pages 1143-1158, Sept. 1994.

  
  

• Combinationality

  S. Malik. Analysis of Cyclic Combinational Circuits. in Proc. Int'l Conf. on Computer-Aided Design, 1993.

  J.-H. R. Jiang, A. Mishchenko, and R. Brayton. On Breakable Cyclic Definitions. in Proc. Int'l Conf. on Computer-Aided Design, pages 411-418, San Jose, USA, November 2004.

  
  

• Technology Mapping

  K. Keutzer. DAGON: Technology Binding and Local Optimization by DAG Matching. in Proc. Design Automation Conf., pages 341-347, 1987.

  E. Lehman, Y. Watanabe, J. Grodstein, and H. Harkness. Logic Decomposition During Technology Mapping. IEEE Transactions on Computer-Aided Design, pages 813-834, August 1997.

  
  

• Retiming

  C. E. Leiserson and J. B. Saxe. Optimizing synchronous systems. Journal of VLSI and Computer Systems, 1(1):41--67, Spring
  1983.

  C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, vol. 6, pages 5--35, 1991.

  
  

• Synthesis System

  E. Sentovich et al. SIS: A System for Sequential Circuit Synthesis. Memorandum No. UCB/ERL M92/41, University of California at Berkeley, 1992.

  Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. http://www.eecs.berkeley.edu/~alanmi/abc/

  
  

• Model Checking

  K. L. McMillan. Interpolation and SAT-based Model Checking. In Proc. CAV, 2003.

  A. R. Bradley. SAT-based Model Checking without Unrolling. In Proc. VMCAI, 2011.