Compacting Intermediate States

1. Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Formal verification using parametric representations of Boolean constraints. In DAC, Proceedings of Design Automation Conference, pages 402–407, June 1999.

   Google Scholar 

2. Robert L. Ashenhurst. The decomposition of switching functions. In Proceedings of the International Symposium on the Theory of Switching, Part I 29, pages 74–116, 1957.

   Google Scholar 

3. Franc Brglez, David Bryan, and Krzysztof Koźmiński. Combinational profiles of sequential benchmark circuits. In ISCAS, Proceedings of the International Symposyium on Circuits and Systems, pages 1929–1934, May 1989.

   Google Scholar 

4. Valeria Bertacco and Maurizio Damiani. Boolean function representation based on disjoint-support decompositions. In ICCD, Proceedings of the International Conference on Computer Design, pages 27–33, October 1996.

   Google Scholar 

5. Valeria Bertacco and Maurizio Damiani. Boolean function representation using parallel-access diagrams. In Proceedings of the Sixth Great Lakes Symposium on VLSI, March 1996.

   Google Scholar 

6. Valeria Bertacco and Maurizio Damiani. The disjunctive decomposition of logic functions. In ICCAD, Proceedings of the International Conference on Computer Aided Design, pages 78–82, November 1997.

   Google Scholar 

7. Valeria Bertacco, Maurizio Damiani, and Stefano Quer. Cycle-based symbolic simulation of gate-level synchronous circuits. In DAC, Proceedings of Design Automation Conference, pages 391–396, June 1999.

   Google Scholar 

8. Valeria Bertacco. Achieving Scalable Hardware Verification with Symbolic Simulation. PhD thesis, Stanford University, 2003.

   Google Scholar 

9. Robert K. Brayton and Curt McMullen. The decomposition and factorization of Boolean expressions, In ISCAS, Proceedings of the International Symposyium on Circuits and Systems, pages 49–54, 1982.

   Google Scholar 

10. Valeria Bertacco and Kunle Olukotun. Efficient state representation for symbolic simulation. In DAC, Proceedings of Design Automation Conference, June 2002.

    Google Scholar 

11. Karl Brace, Richard Rudell, and Randal E. Bryant. Efficient implementation of a BDD package. In DAC, Proceedings of Design Automation Conference, pages 40–45, 1990.

    Google Scholar 

12. Robert K. Brayton, Richard Rudell, Alberto Sangiovanni-Vincentelli, and Albert R. Wang. MIS: A multiple-level logic optimization system. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 6(6): 1062–1081, November 1987.

    Article  Google Scholar 

13. Olivier Coudert, Christian Berthet, and Jean Christophe Madre. Verification of synchronous sequential machines based on symbolic execution. In Automatic Verification Methods for Finite State Systems, International Workshop, volume 407 of Lecture Notes in Computer Science, pages 365–3. Springer, June 1989.

    Google Scholar 

14. Olivier Coudert and Jean Christophe Madre. A unified framework for the formal verification of sequential circuits. In ICCAD, Proceedings of the International Conference on Computer Aided Design, pages 126–129, November 1990.

    Google Scholar 

15. Olivier Coudert and Jean Christophe Madre. Implicit and incremental computation of primes and essential primes of Boolean functions. In DAC, Proceedings of Design Automation Conference, pages 36–39, June 1992.

    Google Scholar 

16. Herbert A. Curtis. A New Approach to the Design of Switching Circuits. Van Nostrand, Princeton, N.J., 1962.

    Google Scholar 

17. Alan J. Hu and David L. Dill. Reducing BDD size by exploiting functional dependencies. In DAC, Proceedings of Design Automation Conference, pages 266–271, June 1993.

    Google Scholar 

18. Prabhat Jain and Ganesh Gopalakrishnan. Some techniques for efficient symbolic simulation-based verification. In ICCD, Proceedings of the International Conference on Computer Design, pages 598–602, October 1992.

    Google Scholar 

19. Prabhat Jain and Ganesh Gopalakrishnan. Hierarchical constraint solving in the parametric form with applications to efficient symbolic simulation based verification. In ICCD, Proceedings of the International Conference on Computer Design, pages 304–307, October 1993.

    Google Scholar 

20. Prabhat Jain and Ganesh Gopalakrishnan. Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13:1005–1015, August 1994.

    Article  Google Scholar 

21. Richard M. Karp. Functional decomposition and switching circuit design. Journal of the Society for Industrial and Applied Mathematics, 11(2):291–335, 1963.

    Article  MATH  MathSciNet  Google Scholar 

22. Kevin Karplus. Representing Boolean functions with if-then-else dags. Technical Report UCSC-CRL-88-28, Baskin Center for Computer Engineering & Information Sciences, 1988.

    Google Scholar 

23. Kevin Karplus. Using if-then-else dags for multi-level logic minimization. In Proceedings of Advanced Research in VLSI, pages 101–118, 1989.

    Google Scholar 

24. Kevin Karplus. Using if-then-else dags to do technology mapping for field-programmable gate arrays. Technical Report UCSC-CRL-90-43, Baskin Center for Computer Engineering & Information Sciences, 1990.

    Google Scholar 

25. In-Ho Moon, Hee Hwan Kwak, James Kukula, Thomas Shiple, and Carl Pixley. Simplifying circuits for formal verification using parametric representation. In FMCAD, Proceedings of International Conference on Formal Methods in Computer-Aided Design, pages 52–69. Springer-Verlag, 2002.

    Google Scholar 

26. Rajeev Murgai, Yoshihito Nishizaki, Narendra V. Shenoy, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli. Logic synthesis for programmable gate arrays. In DAC, Proceedings of Design Automation Conference, pages 620–625, June 1990.

    Google Scholar 

27. Patrick C. McGeer, Jagesh V. Sanghavi, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli. ESPRESSO-SIGNATURE: A new exact minimizer for logic functions. In DAC, Proceedings of Design Automation Conference, pages 618–624, June 1993.

    Google Scholar 

28. Stephen Plaza and Valeria Bertacco. Boolean operations on decomposed functions. In International Workshop on Logic Synthesis, pages 310–317, June 2005.

    Google Scholar 

29. Stephen Plaza and Valeria Bertacco. STACCATO: Disjoint support decompositions from BDDs through symbolic kernels. In ASPDAC, Proceedings of the Asia South Pacific Design Automation Conference, pages 276–279, January 2005.

    Google Scholar 

30. Tsutomu Sasao. Totally undecomposable functions: Applications to efficient multiple-valued decompositions. In ISMVL, pages 59–65, 1999.

    Google Scholar 

31. Claude E. Shannon. The synthesis of two-terminal switching circuits. Bell Systems Technical Journal, 28(1):59–98, 1949.

    MathSciNet  Google Scholar 

32. Theodore Singer. The decomposition chart as a theoretical aid. Technical Report BL-4, Sec.III, Harvard Computational Laboratory, 1953.

    Google Scholar 

33. Tsutomu Sasao and Munehiro Matsuura. DECOMPOS: An integrated system for functional decomposition. In International Workshop on Logic Synthesis, pages 471–477, 1998.

    Google Scholar 

34. V. Yun-Shen Shen, Archie C. McKellar, and Peter Weiner. A fast algorithm for the disjunctive decomposition of switching functions. IEEE Transactions on Computers, C-20(3):304–309, 1971.

    Google Scholar 

35. C. A. J. van Eijk and Jochen A. G. Jess. Exploiting functional dependencies in finite state machine verification. In ED&TC, Proceedings of the European Design and Test Conference, pages 9–14, March 1996.

    Google Scholar 

36. Saeyang Yang. Logic synthesis and optimization benchmarks user guide, version 3.0. Technical report, Microelectronics Center of North Carolina, January 1991.

    Google Scholar 

Download references