Method for verifying and representing hardware by decomposition and partitioning
AssigneeFujitsu Limited
InventorJawahar Jain
Life of this patent
Estimating the term…
Abstract
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.
Claims20
A computer-implemented method of determining if first and second circuits, each with a set of corresponding common primary inputs and corresponding common primary outputs, are equivalent, comprising:
- representing the first circuit as a first Boolean function;
- representing the second circuit as a second Boolean function;
- representing a Boolean space by exclusive ORinq the corresponding primary outputs of the first and second Boolean functions;
- building a decomposed first Binary Decision Diagram for the Boolean space;
- partitioning the Boolean space into first and second partitions during composition of a decomposition point when the Binary Decision Diagram resulting from composition exceeds a predetermined constraint on computer memory usage;
- and
- determining if the first and second partitions are zero;
- wherein determining if the first and second partitions result to zero includes:
- partitioning the first partition into a plurality of first partitions;
- building Binary Decision Diagrams for each of the first partitions unless a predetermined constraint on memory usage is exceeded;
- building a decomposed partition string having components for at least one of the first partitions for which the predetermined constraint on memory usage was exceeded;
- and
- combining the components in a scheduled order until a combination of components is zero.
A method of evaluating a digital system comprising:
- representing the digital system as a Boolean function, the Boolean function forming a Boolean space;
- partitioning the Boolean space into first and second partitions;
- forming a decomposed partition string having elements, the decomposed partition string representing the first partition;
- and
- ordering the elements of the decomposed partition string into a scheduling order;
- combining the elements according to the scheduling order.
A computer-implemented method of verifying a combinatorial circuit having primary inputs to which values are assignable, the primary inputs forming input vectors when the primary inputs are assigned varying values, comprising the steps of:
- partitioning a Boolean space representation of the combinatorial circuit into multiple windows, no two windows sharing a common input vector;
- executing an ordered BDD-based verification technique on each window to determine a verification result until a verification result is obtained or predetermined sets of constraints on computer memory usage are exceeded;
- forming a decomposed partition string for each window for which the predetermined sets of constraints on computer memory usage are exceeded, the decomposed partition string being of a combination of elements;
- combining the elements in a scheduled order and determining after each combination whether the decomposed partition string is zero.
A method of evaluating a digital system comprising:
- representing the digital system as a Boolean function, the Boolean function forming a Boolean space;
- recursively partitioning the Boolean space into partitions;
- forming a decomposed partition string having components, the decomposed partition string representing at least one partition
- executing an ordered BDD-based verification technique on at least one partition not represented by a decomposed partition string;
- and
- sequentially combining the components of the decomposed partition string in a scheduled order.
A system for evaluating a digital circuit comprising:
- means for representing the digital circuit as a Boolean function, the Boolean function forming a Boolean space;
- means for partitioning the Boolean space into first and second partitions;
- means for forming a decomposed partition string having elements, the decomposed partition string representing the first partition
- means for ordering the elements of the decomposed partition string into a scheduling order;
- and
- means for combining the elements according to the scheduling order.
Dependencies are inferred from the claim text.