Abstract

In this paper, we review various real-life CAD-related problems that can be formulated with Boolean reasonings. The problems listed are all important ones in CAD for digital systems. Everything in logic design is relating to Boolean functions and many of them have been solved by applying Boolean reasoning techniques, such as logic expression simplification, Boolean function manipulation, etc.
However, there are still many problems in CAD for digital systems that could be solved effectively and efficiently by Boolean reasoning. Here we will list them up with examples and discuss what are the key issues in terms of practicalness when we try to solve them with Boolean reasoning. We also show some initial research activities in attacking those problems.
The topics shown here are:

• Logic synthesis/optimization issues
  • Logic circuit optimization and redesign by formulation with Boolean unification
  • Engineering change problems in logic synthesis with quantified Boolean formulae
  • AND-EOR minimization and other logic optimization with Boolean unification
• Logic verification issues
  • Problems related to Boolean comparison: Flip-flop matching and Boolean comparison with internal don't cares
  • SAT based model checking and its variants
  • High level verification with uninterpreted functions

Once some of them are solved with practical performance, they are sure to be used in practical design environment for digital systems, and influence a lot in terms of quality of such designs.
In this paper we will concentrate only on logic synthesis field. In the actual presentation, we will give details on all of the above.