Efficient solution of systems of Boolean equations

ABSTRACT

This paper describes an algorithm for the efficient solution of large systems of Boolean equations. The algorithm exploits the fact that, in some cases, the composition operation of Boolean functions represented by BDD's can be performed in a very efficient manner. Thus, the algorithm tries to eliminate as many variables and equations as possible through function composition. When the system can no longer be reduced in this way, the elimination process is continued through the use of Shannon decomposition. Numerical results show that the performance of this algorithm is significantly superior to that of a previous algorithm proposed by the authors.

REFERENCES

• 1: S. Devadas and A. R. Newton, "Exact Algorithms for Output Encoding, State Assignment, and Four- Level Boolean Minimization", IEEE Transactions on Computer-Aided Design, vol. 10, no. 1, pp. 13-27, January 1991.
• 2: E C. McGeer, A. Saldanha, E R. Stephan, R. K. Brayton, and A. Sangiovanni-Vincentelli, "Timing Analysis and Delay-Fault Test Generation using Path- Recursive Funcions", in Proceedings of the 1991 International Conference on Computer-Aided Design, Santa Clara, CA, November 1991, pp. 180-183.
• 3: T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability", IEEE Transactions on Computer- Aided Design, vol. 11, no. 1, pp. 4-15, January 1992.
• 4: Scott Woods , Giorgio Casinovi, Gate-level simulation of digital circuits using multi-valued Boolean algebras, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.413-419, November 05-09, 1995, San Jose, California, United States
• 5: R. E. Tarjan, "Depth-first search and linear graph algorithms", SlAM Journal on Computing, vol. 1, pp. 146-160, 1972.
• 6: Sergiu Rudeanu, Boolean Functions and Equations, North-Holland Publishing Co., Amsterdam, 1974.
• 7: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 8: M. Fujita, H. Fujisawa, and N. Kawato, "Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagram", in Proceedings of the 1988 International Conference on Computer- Aided Design, Santa Clara, CA, November 1988, pp. 2-5.
• 9: Sharad Malik, Albert R. Wang, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli, "Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment", in Proceedings of the 1988 International Conference on Computer-AidedDesign, Santa Clara, CA, November 1988, pp. 6-9.
• 10: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Combinational logic

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Experimentation, Theory

Keywords:
Boolean equations solution, gate-level logic simulation.