# US 2020/0394352 A1 · Satisfiability sweeping for synthesis

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 2020/0394352 A1
- Document ID: US20200394352A1
- Status: Published application
- Kind: A1
- Application number: 16/904,077
- Filed: 2020-06-17
- Published: 2020-12-17
- Earliest claimed: 2019-06-17
- Assignees: Synopsys, Inc.
- Applicants: Synopsys, Inc.
- Inventors: Luca Gaetano AMARU; Jiong LUO; Patrick VUILLOD
- Web page: https://patentgrep.com/patent/US20200394352A1

## CPC

- G06F 30/327: Logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist
- G06F 30/31: Design entry, e.g. editors specifically adapted for circuit design
- G06F 2119/16: Equivalence checking
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## 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.

## Claims

### Claim 1

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.

### Claim 2 (depends on 1)

The method of claim 1, wherein selecting the first driver gate is based on a topological and polarity ordering of the first subset of the plurality of gates.

### Claim 3 (depends on 2)

The method of claim 2, wherein merging the first candidate gate and the first driver gate comprises:
determining a local input connected to a local output of the first candidate gate; and
inserting a connection in the integrated circuit design between a local output of the first driver gate and the local input.

### Claim 4 (depends on 3)

The method of claim 3, wherein the connection comprises an inverter gate in response to the first driver gate being a complementation of the first candidate gate.

### Claim 5 (depends on 1)

The method of claim 1, further comprising:
selecting a second candidate gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determining a second subset of the plurality of gates belonging to a second gate class comprising the second candidate gate;
selecting a second driver gate from the second subset of the plurality of gates based on a topological and polarity ordering of the second subset of gates;
obtaining a counter-example simulation pattern after calling the SAT-solver based on the second candidate gate and the second driver gate;
executing an incremental simulation of the integrated circuit design based on the counter-example simulation pattern; and
determining a refined second subset of the plurality of gates by removing at least the second driver gate from the second subset of the plurality of gates based on the incremental simulation.

### Claim 6 (depends on 5)

The method of claim 5, further comprising:
selecting a third driver gate from the refined second subset of the plurality of gates;
obtaining a second confirmed equivalence by calling the SAT-solver based on the second candidate gate and the third driver gate; and
modifying, based on the second confirmed equivalence, the integrated circuit design by merging the second candidate gate and the third driver gate.

### Claim 7 (depends on 1)

The method of claim 1, further comprising:
selecting a second candidate gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determining a second subset of the plurality of gates belonging to a second gate class comprising the second candidate gate;
selecting a second driver gate from the second subset of the plurality of gates;
obtaining an undeterminable (unDET) response after calling the SAT-solver based on the second candidate gate and the second driver gate; and
marking the second candidate gate as excluded based on the unDET response.

### Claim 8 (depends on 1)

The method of claim 1, wherein inputting the plurality of simulation patterns comprises:
inputting a plurality of random simulation patterns to the plurality of gates;
selecting a first test gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determining a toggle rate of a local output of the test gate;
executing a comparison of the toggle rate with a toggle threshold;
determining, based on the comparison, a next bit for the local output of the test gate that increases the toggle rate;
determining an additional simulation pattern by calling another SAT-solver based on the next bit and the plurality of gates; and
incrementally simulating the plurality of gates based on the additional simulation pattern to trigger the next bit at the local output of the test gate.

### Claim 9 (depends on 1)

The method of claim 1, wherein inputting the plurality of simulation patterns further comprises:
determining an auxiliary simulation pattern that has Hamming distance 1 from the additional simulation pattern; and
incrementally simulating the plurality of gates based on the auxiliary simulation pattern.

### Claim 10

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.

### Claim 11 (depends on 10)

The system of claim 10, wherein merging the first candidate gate and the first driver gate comprises:
determining a local input connected to a local output of the first candidate gate; and
inserting a connection in the integrated circuit design between a local output of the first driver gate and the local input,
wherein the connection comprises an inverter gate in response to the first driver gate being a complementation of the first candidate gate, and
wherein selecting the first driver gate is based on a topological and polarity ordering of the first subset of the plurality of gates.

### Claim 12 (depends on 10)

The system of claim 10, wherein the instructions, when executed, further cause the processor to:
select a second candidate gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determine a second subset of the plurality of gates belonging to a second gate class comprising the second candidate gate;
select a second driver gate from the second subset of the plurality of gates based on a topological and polarity ordering of the second subset of gates;
obtain a counter-example simulation pattern after calling the SAT-solver based on the second candidate gate and the second driver gate;
execute an incremental simulation of the integrated circuit design based on the counter-example simulation pattern; and
determine a refined second subset of the plurality of gates by removing at least the second driver gate from the second subset of the plurality of gates based on the incremental simulation.

### Claim 13 (depends on 12)

The system of claim 12, wherein the instructions, when executed, further cause the processor to:
select a third driver gate from the refined second subset of the plurality of gates;
obtain a second confirmed equivalence by calling the SAT-solver based on the second candidate gate and the third driver gate; and
modify, based on the second confirmed equivalence, the integrated circuit design by merging the second candidate gate and the third driver gate.

### Claim 14 (depends on 10)

The system of claim 10, wherein the instructions, when executed, further cause the processor to:
select a second candidate gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determine a second subset of the plurality of gates belonging to a second gate class comprising the second candidate gate;
select a second driver gate from the second subset of the plurality of gates;
obtain an undeterminable (unDET) response after calling the SAT-solver based on the second candidate gate and the second driver gate; and
mark the second candidate gate as excluded based on the unDET response.

### Claim 15 (depends on 10)

The system of claim 10, wherein inputting the plurality of simulation patterns comprises:
inputting a plurality of random simulation patterns to the plurality of gates;
selecting a first test gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determining a toggle rate of a local output of the test gate;
executing a comparison of the toggle rate with a toggle threshold;
determining, based on the comparison, a next bit for the local output of the test gate that increases the toggle rate;
determining an additional simulation pattern by calling another SAT-solver based on the next bit and the plurality of gates;
determining an auxiliary simulation pattern that has Hamming distance 1 from the additional simulation pattern; and
incrementally simulating the plurality of gates based on the additional simulation pattern and the auxiliary simulation pattern.

### Claim 16

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.

### Claim 17 (depends on 16)

The non-transitory computer readable medium of claim 16, wherein merging the first candidate gate and the first driver gate comprises:
determining a local input connected to a local output of the first candidate gate; and
inserting a connection in the integrated circuit design between a local output of the first driver gate and the local input,
wherein selecting the first driver gate is based on a topological and polarity ordering of the first subset of the plurality of gates, and
wherein the connection comprises an inverter gate in response to the first driver gate being a complementation of the first candidate gate.

### Claim 18 (depends on 16)

The non-transitory computer readable medium of claim 16, wherein the instructions, when executed, further cause the processor to:
select a second candidate gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determine a second subset of the plurality of gates belonging to a second gate class comprising the second candidate gate;
select a second driver gate from the second subset of the plurality of gates based on a topological and polarity ordering of the second subset of gates;
obtain a counter-example simulation pattern after calling the SAT-solver based on the second candidate gate and the second driver gate;
execute an incremental simulation of the integrated circuit design based on the counter-example simulation pattern;
determine a refined second subset of the plurality of gates by removing at least the second driver gate from the second subset of the plurality of gates based on the incremental simulation;
select a third driver gate from the refined second subset of the plurality of gates;
obtain a second confirmed equivalence by calling the SAT-solver based on the second candidate gate and the third driver gate; and
modify, based on the second confirmed equivalence, the integrated circuit design by merging the second candidate gate and the third driver gate.

### Claim 19 (depends on 10)

The non-transitory computer readable medium of claim 10, wherein the instructions, when executed, further cause the processor to:
select a second candidate gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determine a second subset of the plurality of gates belonging to a second gate class comprising the second candidate gate;
select a second driver gate from the second subset of the plurality of gates;
obtain an undeterminable (unDET) response after calling the SAT-solver based on the second candidate gate and the second driver gate; and
mark the second candidate gate as excluded based on the unDET response.

### Claim 20 (depends on 16)

The non-transitory computer readable medium of claim 16, wherein inputting the plurality of simulation patterns comprises:
inputting a plurality of random simulation patterns to the plurality of gates;
selecting a first test gate from the plurality of gates based on the inverse topological ordering of the plurality of gates;
determining a toggle rate of a local output of the test gate;
executing a comparison of the toggle rate with a toggle threshold;
determining, based on the comparison, a next bit for the local output of the test gate that increases the toggle rate;
determining an additional simulation pattern by calling another SAT-solver based on the next bit and the plurality of gates; and
determining an auxiliary simulation pattern that has Hamming distance 1 from the additional simulation pattern; and
incrementally simulating the plurality of gates based on the additional simulation pattern and the auxiliary simulation pattern.