Satisfiability sweeping for synthesis
AssigneeSynopsys, Inc.
InventorsLuca Gaetano AMARU, Jiong LUO, Patrick VUILLOD
Life of this patent
Estimating the term…
Abstract
A system and method for SAT-sweeping is disclosed. According to one embodiment, a method includes determining gate classes by inputting simulation patterns to gates in an integrated circuit design, selecting a candidate gate based on an inverse topological ordering of the gates, and then selecting a driver gate belonging to the same gate class as the candidate gate. A SAT-solver is called based on the candidate gate and the driver gate to confirm equivalence. The candidate gate and the driver gate are then merged in the integrated circuit design.
Claims20
A method, comprising:
- determining a plurality of gate classes by inputting a plurality of simulation pattern inputs to a plurality of gates in an integrated circuit design;
- selecting a first candidate gate from the plurality of gates based on an inverse topological ordering of the plurality of gates;
- determining a first subset of the plurality of gates belonging to a first gate class comprising the first candidate gate;
- selecting a first driver gate from the first subset of the plurality of gates;
- obtaining a first confirmed equivalence after calling a SAT-solver based on the first candidate gate and the first driver gate;
- and
- modifying, based on the first confirmed equivalence, the integrated circuit design by merging the first candidate gate and the first driver gate.
A system comprising:
- a memory storing instructions;
- and
- a processor, coupled with the memory and to execute the instructions, the instructions when executed cause the processor to:
- determine a plurality of gate classes by inputting a plurality of simulation patterns to a plurality of gates in an integrated circuit design;
- select a first candidate gate from the plurality of gates based on an inverse topological ordering of the plurality of gates;
- determine a first subset of the plurality of gates belonging to a first gate class comprising the first candidate gate;
- select a first driver gate from the first subset of the plurality of gates;
- obtain a first confirmed equivalence after calling a SAT-solver based on the first candidate gate and the first driver gate;
- and
- modify, based on the first confirmed equivalence, the integrated circuit design by merging the first candidate gate and the first driver gate.
A non-transitory computer readable medium comprising stored instructions, which when executed by a processor, cause the processor to:
- determine a plurality of gate classes by inputting a plurality of simulation patterns to a plurality of gates in an integrated circuit design;
- select a first candidate gate from the plurality of gates based on an inverse topological ordering of the plurality of gates;
- determine a first subset of the plurality of gates belonging to a first gate class comprising the first candidate gate;
- select a first driver gate from the first subset of the plurality of gates;
- obtain a first confirmed equivalence after calling a SAT-solver based on the first candidate gate and the first driver gate;
- and
- modify, based on the first confirmed equivalence, the integrated circuit design by merging the first candidate gate and the first driver gate.
Dependencies are inferred from the claim text.