Verification of digital circuitry using range generators

An article of manufacture comprising:

• a machine-accessible medium including data that, when accessed by a machine, causes the machine to perform operations comprising:
• constructing an exact range generator (RG) represented by a characteristic function of a range of a cut function for a first cut circuit in an implementation circuit and a second cut circuit in a reference circuit, the exact range generator being simpler than the first and second cut circuits and having a RG range identical to the range of the cut function;
• and
• checking equivalence of the implementation circuit and the reference circuit using the exact range generator.

An article of manufacture comprising:

• a machine-accessible medium including data that, when accessed by a machine, causes the machine to perform operations comprising:
• constructing an superset range generator (SRG) represented by a characteristic function of a range of a cut function for a first cut circuit in an implementation circuit and a second cut circuit in a reference circuit, the SRG being simpler than the cut circuit and having a SRG range larger than the range of the cut function;
• and
• checking equivalence of the implementation circuit and the reference circuit using the SRG.

A system comprises:

• a processor;
• and
• a memory coupled to the processor containing an electronic design automation (EDA) tool, the EDA tool, when executed, causes the processor to:
• construct an exact range generator (RG) represented by a characteristic function of a range of a cut function for a first cut circuit in an implementation circuit and a second cut circuit in a reference circuit, the exact range generator being simpler than the first and second cut circuits and having a RG range identical to the range of the cut function, and
• check equivalence of the implementation circuit and the reference circuit using the exact range generator.

A system comprising:

• a processor;
• and
• a memory coupled to the processor containing an electronic design automation (EDA) tool, the EDA tool, when executed, causes the processor to:
• construct an superset range generator (SRG) represented by a characteristic function of a range of a cut function for a first cut circuit in an implementation circuit and a second cut circuit in a reference circuit, the SRG being simpler than the cut circuit and having a SRG range larger than the range of the cut function;
• and
• check equivalence of the implementation circuit and the reference circuit using the SRG.