Requirements on Data Structures in Formal Circuit Verification

  • Christoph Meinel
  • Thorsten Theobald


In the previous chapter, we have introduced several representation types for switching functions. In particular, we have described the switching functions under consideration based on the following ideas:
  • by systematically tabulating the function values (e.g., truth tables)

  • by providing a method for computing the function (e.g., disjunctive or conjunctive normal forms, Boolean formulas or circuits)

  • by describing a scheme for evaluating the function (e.g., decision trees, branching programs).


Boolean Operation Representation Type Finite State Machine Truth Table Conjunctive Normal Form 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. The mentioned logic synthesis systems are described in the following references: MINI [HC074], ESPRESSO [BHMS84], MIS [BRSW87], BOLD [HLJ+89] and SIS [SSM+92]. Discussions concerning the requirements on data structures in formal circuit verification can also be found in the surveys [Bry92, Weg94, MT98].Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Christoph Meinel
    • 1
  • Thorsten Theobald
    • 2
  1. 1.University of TrierTrierGermany
  2. 2.Technical University MünchenMünchenGermany

Personalised recommendations