Scalable don't-care-based logic optimization and resynthesis

ABSTRACT

We describe an optimization method for combinational and sequential logic networks, with emphasis on scalability and the scope of optimization. The proposed resynthesis (a) is capable of substantial logic restructuring, (b) is customizable to solve a variety of optimization tasks, and (c) has reasonable runtime on industrial designs. The approach uses don't cares computed for a window surrounding a node and can take into account external don't cares (e.g. unreachable states). It uses a SAT solver and interpolation to find a new representation for a node. This representation can be in terms of inputs from other nodes in the window thus effecting Boolean re-substitution. Experimental results on 6-input LUT networks after high effort synthesis show substantial reductions in area and delay. When applied to 20 large academic benchmarks, the LUT count and logic level is reduced by 45.0% and 12.2%, respectively. The longest runtime for synthesis and mapping is about two minutes. When applied to a set of 14 industrial benchmarks ranging up to 83K 6-LUTs, the LUT count and logic level is reduced by 11.8% and 16.5%, respectively. Experimental results on 6-input LUT networks after high-effort synthesis show substantial reductions in area and delay. The longest runtime is about 30 minutes.

REFERENCES

• 1: Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification, Release 80802. http://www.eecs.berkeley.edu/~alanmi/abc/
• 2: Per Bjesse , Koen Claessen, SAT-Based Verification without State Space Traversal, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.372-389, November 01-03, 2000
• 3: M. L. Case, A. Mishchenko, and R. K. Brayton, "Inductively finding a reachable state space over-approximation", Proc. IWLS '06, pp. 172--179. http://www.eecs.berkeley.edu/~alanmi/publications/2006/iwls06_inv.pdf
• 4: M. L. Case, A. Mishchenko, and R. K. Brayton, "Cut-based inductive invariant computation", Proc. IWLS'08, pp. 253--258. http://www.eecs.berkeley.edu/~alanmi/publications/2008/iwls08_ind.pdf
• 5: Kai-Hui Chang , I. L. Markov , V. Bertacco, Fixing Design Errors with Counterexamples and Resynthesis, Proceedings of the 2007 conference on Asia South Pacific design automation, p.944-949, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358111]
• 6: Kuang-Chien Chen , Jason Cong, Maximal reduction of lookup-table based FPGAs, Proceedings of the conference on European design automation, p.224-229, November 1992, Congress Centrum Hamburg, Hamburg, Germany
• 7: Jason Cong , Yizhou Lin , Wangning Long, SPFD-based global rewiring, Proceedings of the 2002 ACM/SIGDA tenth international symposium on Field-programmable gate arrays, February 24-26, 2002, Monterey, California, USA [doi>10.1145/503048.503060]
• 8: D. Chen , J. Cong, DAOmap: a depth-optimal area optimization mapping algorithm for FPGA designs, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.752-759, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382677]
• 9: N. Een and N. Sörensson, "An extensible SAT-solver". SAT '03. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
• 10: Evgueni Goldberg , Yakov Novikov, Verification of Proofs of Unsatisfiability for CNF Formulas, Proceedings of the conference on Design, Automation and Test in Europe, p.10886, March 03-07, 2003
• 11: Victor N. Kravets , Prabhakar Kudva, Implicit enumeration of structural changes in circuit optimization, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996691]
• 12: Chih-Chun Lee , Jie-Hong R. Jiang , Chung-Yang (Ric) Huang , Alan Mishchenko, Scalable exploration of functional dependency by interpolation and incremental SAT solving, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
• 13: K.L. McMillan, "Interpolation and SAT-based model checking". Proc. CAV '03, pp. 1--13, LNCS 2725, Springer, 2003.
• 14: K. McMillan, "Don't-care computation using k-clause approximation", Proc. IWLS '05, pp. 153--160.
• 15: Alan Mishchenko , Bernd Steinbach , Marek Perkowski, An algorithm for bi-decomposition of logic functions, Proceedings of the 38th conference on Design automation, p.103-108, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378353]
• 16: Alan Mishchenko , Robert K. Brayton, SAT-Based Complete Don't-Care Computation for Network Optimization, Proceedings of the conference on Design, Automation and Test in Europe, p.412-417, March 07-11, 2005 [doi>10.1109/DATE.2005.264]
• 17: A. Mishchenko and R. K. Brayton, "Scalable logic synthesis using a simple circuit structure", Proc. IWLS '06, pp. 15--22. http://www. eecs.berkeley.edu/~alanmi/publications/2006/iwls06_sls.pdf
• 18: Alan Mishchenko , Satrajit Chatterjee , Robert Brayton, DAG-aware AIG rewriting a fresh look at combinational logic synthesis, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147048]
• 19: A. Mishchenko, J. S. Zhang, S. Sinha, J. R. Burch, R. Brayton, and M. Chrzanowska-Jeske, "Using simulation and satisfiability to compute flexibilities in Boolean networks", IEEE T CAD, Vol. 25(5), May 2006, pp. 743--755. http://www.eecs.berkeley.edu/~alanmi/publications/2005/tcad05_s&s.pdf
• 20: Alan Mishchenko , Satrajit Chatterjee , Robert Brayton , Niklas Een, Improvements to combinational equivalence checking, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233679]
• 21: A. Mishchenko, S. Chatterjee, and R. Brayton, "Improvements to technology mapping for LUT-based FPGAs". IEEE TCAD, Vol. 26(2), Feb 2007, pp. 240--253. http://www.eecs.berkeley.edu/~alanmi/publications/2006/tcad06_map.pdf
• 22: Alan Mishchenko , Sungmin Cho , Satrajit Chatterjee , Robert Brayton, Combinational and sequential mapping with priority cuts, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
• 23: Alan Mishchenko , Robert Brayton , Satrajit Chatterjee, Boolean factoring and decomposition of logic networks, Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, November 10-13, 2008, San Jose, California
• 24: S. Muroga , Y. Kambayashi , H. C. Lai , J. N. Culliney, The Transduction Method-Design of Logic Networks Based on Permissible Functions, IEEE Transactions on Computers, v.38 n.10, p.1404-1424, October 1989 [doi>10.1109/12.35836]
• 25: Peichen Pan , Chih-Chang Lin, A new retiming-based technology mapping algorithm for LUT-based FPGAs, Proceedings of the 1998 ACM/SIGDA sixth international symposium on Field programmable gate arrays, p.35-42, February 22-25, 1998, Monterey, California, United States [doi>10.1145/275107.275118]
• 26: Stephen M. Plaza , Kai-hui Chang , Igor L. Markov , Valeria Bertacco, Node Mergers in the Presence of Don't Cares, Proceedings of the 2007 conference on Asia South Pacific design automation, p.414-419, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358021]
• 27: Nikhil Saluja , Sunil P. Khatri, A robust algorithm for approximate compatible observability don't care (CODC) computation, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996688]
• 28: Hamid Savoj, Don't cares in multi-level network optimization, University of California at Berkeley, Berkeley, CA, 1992
• 29: E. Sentovich et al. "SIS: A system for sequential circuit synthesis." Technical Report, UCB/ERI, M92/41, ERL, Dept. of EECS, UC Berkeley, 1992.
• 30: Yu-Shen Yang , S. Sinha , A. Veneris , R. K. Brayton, Automating Logic Rectification by Approximate SPFDs, Proceedings of the 2007 conference on Asia South Pacific design automation, p.402-407, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358019]
• 31: Qi Zhu , Nathan Kitchen , Andreas Kuehlmann , Alberto Sangiovanni-Vincentelli, SAT sweeping with local observability don't-cares, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1146970]
• 32: Xilinx Virtex-5 Product Table, http://www.xilinx.com/products/silicon_solutions/fpgas/virtex/virtex5/v5product_table.pdf
• 33: Xilinx Stratix IV FPGA Family Overview, http://www.altera.com/products/devices/stratix-fpgas/stratix-iv/overview/stxiv-overview.html

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Optimization

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Automatic synthesis
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Gate arrays

General Terms:
Algorithms, Experimentation, Performance

Keywords:
boolean satisfiability, fpga, interpolation, logic optimization, technology mapping, windowing