Requirements on Data Structures in Formal Circuit Verification
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).
KeywordsBoolean Operation Representation Type Finite State Machine Truth Table Conjunctive Normal Form
Unable to display preview. Download preview PDF.
- 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