A system and method for representing digital circuits and systems in
multiple partitions of Boolean space, and for performing digital circuit
or system validation using the multiple partitions. Decision diagrams are
built for the digital circuit or system and pseudo-variables are
introduced at decomposition points to reduce diagram size.
Pseudo-variables remaining after decomposition are composed and
partitioned to represent the digital circuit or system as multiple
partitions of Boolean space. Each partition is built in a scheduled
order, and is manipulable separately from other partitions.