Skip to content

Commit

Permalink
Optimise reset insertion for mapped gates
Browse files Browse the repository at this point in the history 
Closes workcraft#1649
  • Loading branch information
@danilovesky
danilovesky committed Oct 17, 2024
1 parent ec5ebac commit 552a278
Show file tree
Hide file tree
Showing 2 changed files with 80 additions and 164 deletions.
16 changes: 8 additions & 8 deletions ci/reset-circuit-charge/charge-tm.circuit.stat.ref
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
Initialisation check: true
Combined check: true
Circuit analysis:
Component count (mapped + unmapped) - 16 (16 + 0)
Area - 176.0 + C2R
Non-trivial component count (function + blackbox) - 8 (8 + 0)
Component count (mapped + unmapped) - 15 (15 + 0)
Area - 164.0 + C2R
Non-trivial component count (function + blackbox) - 7 (7 + 0)
Trivial gate count (buffer / 0-delay + inverter / 0-delay + const) - 8 (2 / 0 + 6 / 5 + 0)
Driver pin count (combinational + sequential + undefined) - 16 (15 + 1 + 0)
Literal count combinational / sequential (set + reset) - 30 / 6 (3 + 3)
Driver pin count (combinational + sequential + undefined) - 15 (14 + 1 + 0)
Literal count combinational / sequential (set + reset) - 29 / 6 (3 + 3)
Port count (input + output) - 11 (6 + 5)
Max fanin / fanout - 4 / 4
Fanin distribution [0 / 1 / 2 ...] - 0 / 8 / 3 / 1 / 4
Fanout distribution [0 / 1 / 2 ...] - 0 / 11 / 8 / 1 / 2
Max fanin / fanout - 5 / 4
Fanin distribution [0 / 1 / 2 ...] - 0 / 8 / 2 / 1 / 3 / 1
Fanout distribution [0 / 1 / 2 ...] - 0 / 10 / 8 / 1 / 2
Isolated components / ports / pins - 0 / 0 / 0
228 changes: 72 additions & 156 deletions workcraft/CircuitPlugin/src/org/workcraft/plugins/circuit/utils/ResetUtils.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,10 @@
import org.workcraft.Framework;
import org.workcraft.dom.Node;
import org.workcraft.dom.hierarchy.NamespaceHelper;
import org.workcraft.dom.references.Identifier;
import org.workcraft.dom.references.ReferenceHelper;
import org.workcraft.formula.*;
import org.workcraft.formula.workers.BooleanWorker;
import org.workcraft.formula.workers.CleverBooleanWorker;
import org.workcraft.formula.workers.DumbBooleanWorker;
import org.workcraft.gui.Toolbox;
import org.workcraft.gui.properties.PropertyHelper;
import org.workcraft.plugins.circuit.*;
Expand All @@ -17,6 +15,7 @@
import org.workcraft.plugins.circuit.genlib.LibraryManager;
import org.workcraft.plugins.circuit.tools.InitialisationAnalyserTool;
import org.workcraft.types.Pair;
import org.workcraft.types.Triple;
import org.workcraft.utils.DialogUtils;
import org.workcraft.utils.SortUtils;
import org.workcraft.utils.TextUtils;
Expand All @@ -25,7 +24,6 @@

public final class ResetUtils {

private static final BooleanWorker DUMB_WORKER = DumbBooleanWorker.getInstance();
private static final BooleanWorker CLEVER_WORKER = CleverBooleanWorker.getInstance();
private static final String VERIFICATION_RESULT_TITLE = "Verification result";

Expand Down Expand Up @@ -205,18 +203,7 @@ public static boolean insertReset(VisualCircuit circuit, boolean isActiveLow) {
return false;
}
for (VisualFunctionComponent component : resetComponents) {
if (component.isBuffer()) {
resetBuffer(circuit, component, resetPort, isActiveLow);
} else if (component.isInverter()) {
resetInverter(circuit, component, resetPort, isActiveLow);
} else {
VisualFunctionContact resetContact = CircuitUtils.getFunctionContact(circuit, component, portName);
if (resetContact == null) {
resetComponent(circuit, component, resetPort, isActiveLow);
} else {
CircuitUtils.connectIfPossible(circuit, resetPort, resetContact);
}
}
insertReset(circuit, component, resetPort, isActiveLow);
}
SpaceUtils.positionPort(circuit, resetPort, false);
CircuitUtils.detachJoint(circuit, resetPort, 0.5);
Expand All @@ -225,139 +212,94 @@ public static boolean insertReset(VisualCircuit circuit, boolean isActiveLow) {
}

public static boolean hasForcedInitOutput(CircuitComponent component) {
for (Contact outputContact : component.getOutputs()) {
if (outputContact.getForcedInit()) {
return true;
}
}
return false;
return component.getOutputs().stream().anyMatch(Contact::getForcedInit);
}

private static VisualFunctionComponent resetBuffer(VisualCircuit circuit, VisualFunctionComponent component,
VisualFunctionContact resetPort, boolean activeLow) {
private static boolean insertReset(VisualCircuit circuit, VisualFunctionComponent component,
VisualFunctionContact resetPort, boolean isActiveLow) {

VisualFunctionContact outputContact = component.getFirstVisualOutput();
if ((outputContact == null) || !outputContact.getForcedInit()) {
return null;
if (insertResetIntoMappedCombinationalGate(circuit, component, resetPort, isActiveLow)) {
return true;
}

String gateName = "";
String in1Name = "AN";
String in2Name = "B";
String outName = "ON";

FreeVariable in1Var = new FreeVariable(in1Name);
FreeVariable in2Var = new FreeVariable(in2Name);
BooleanFormula formula = getResetBufferFormula(activeLow, outputContact.getInitToOne(), in1Var, in2Var);
Pair<Gate, Map<BooleanVariable, String>> mapping = GenlibUtils.findMapping(formula, LibraryManager.getLibrary());
if (mapping != null) {
Gate gate = mapping.getFirst();
gateName = gate.name;
Map<BooleanVariable, String> assignments = mapping.getSecond();
in1Name = assignments.get(in1Var);
in2Name = assignments.get(in2Var);
outName = gate.function.name;
}

VisualFunctionContact inputContact = component.getFirstVisualInput();
// Temporary rename gate output, so there is no name clash on renaming gate input
circuit.setMathName(outputContact, Identifier.getTemporaryName());
circuit.setMathName(inputContact, in1Name);
circuit.setMathName(outputContact, outName);
VisualFunctionContact resetContact = circuit.getOrCreateContact(component, in2Name, Contact.IOType.INPUT);
CircuitUtils.connectIfPossible(circuit, resetPort, resetContact);

Contact in1Contact = inputContact.getReferencedComponent();
Contact in2Contact = resetContact.getReferencedComponent();
BooleanFormula setFunction = FormulaUtils.replace(formula, Arrays.asList(in1Var, in2Var),
Arrays.asList(in1Contact, in2Contact));

outputContact.setSetFunction(setFunction);
component.setLabel(gateName);
return component;
}

private static BooleanFormula getResetBufferFormula(boolean activeLow, boolean initToOne,
BooleanVariable in1Var, BooleanVariable in2Var) {

if (initToOne) {
if (activeLow) {
return new Not(new And(new Not(in1Var), in2Var));
} else {
return new Or(in1Var, in2Var);
}
String portName = isActiveLow ? CircuitSettings.getResetActiveLowPort() : CircuitSettings.getResetActiveHighPort();
VisualFunctionContact resetInputPin = CircuitUtils.getFunctionContact(circuit, component, portName);
if (resetInputPin == null) {
appendResetToComponent(circuit, component, resetPort, isActiveLow);
} else {
if (activeLow) {
return new And(in1Var, in2Var);
} else {
return new Not(new Or(new Not(in1Var), in2Var));
}
CircuitUtils.connectIfPossible(circuit, resetPort, resetInputPin);
}
return true;
}

private static VisualFunctionComponent resetInverter(VisualCircuit circuit, VisualFunctionComponent component,
VisualFunctionContact resetPort, boolean activeLow) {
private static boolean insertResetIntoMappedCombinationalGate(VisualCircuit circuit,
VisualFunctionComponent component, VisualFunctionContact resetPort, boolean activeLow) {

VisualFunctionContact outputContact = component.getFirstVisualOutput();
if ((outputContact == null) || !outputContact.getForcedInit()) {
return null;
if (!component.isMapped() || !component.isCombinationalGate()) {
return false;
}
VisualFunctionContact outputPin = component.getGateOutput();
if (outputPin == null) {
return false;
}
BooleanFormula setFunction = outputPin.getSetFunction();
if (setFunction == null) {
return false;
}
FunctionContact resetVar = new FunctionContact(Contact.IOType.INPUT);
BooleanFormula formulaWithReset = getFormulaWithReset(setFunction, resetVar, activeLow, outputPin.getInitToOne());
Triple<Gate, Map<BooleanVariable, String>, Set<String>> extendedMapping = GenlibUtils.findExtendedMapping(
formulaWithReset, LibraryManager.getLibrary(), true, true);

String gateName = "";
String in1Name = "AN";
String in2Name = "B";
String outName = "ON";

FreeVariable in1Var = new FreeVariable(in1Name);
FreeVariable in2Var = new FreeVariable(in2Name);
BooleanFormula formula = getResetInverterFormula(activeLow, outputContact.getInitToOne(), in1Var, in2Var);
Pair<Gate, Map<BooleanVariable, String>> mapping = GenlibUtils.findMapping(formula, LibraryManager.getLibrary());
if (mapping != null) {
Gate gate = mapping.getFirst();
gateName = gate.name;
Map<BooleanVariable, String> assignments = mapping.getSecond();
in1Name = assignments.get(in1Var);
in2Name = assignments.get(in2Var);
outName = gate.function.name;
}

VisualFunctionContact inputContact = component.getFirstVisualInput();
// Temporary rename gate output, so there is no name clash on renaming gate input
circuit.setMathName(outputContact, Identifier.getTemporaryName());
circuit.setMathName(inputContact, in2Name);
circuit.setMathName(outputContact, outName);
VisualFunctionContact resetContact = circuit.getOrCreateContact(component, in1Name, Contact.IOType.INPUT);
CircuitUtils.connectIfPossible(circuit, resetPort, resetContact);

Contact in1Contact = resetContact.getReferencedComponent();
Contact in2Contact = inputContact.getReferencedComponent();
BooleanFormula setFunction = FormulaUtils.replace(formula, Arrays.asList(in1Var, in2Var),
Arrays.asList(in1Contact, in2Contact));

outputContact.setSetFunction(setFunction);
component.setLabel(gateName);
return component;
if (extendedMapping == null) {
return false;
}
// Add reset pin and update gate function
VisualFunctionContact resetInputPin = new VisualFunctionContact(resetVar);
component.addContact(resetInputPin);
outputPin.setSetFunction(formulaWithReset);
// Connect reset pin to reset port proxy
CircuitUtils.connectIfPossible(circuit, resetPort, resetInputPin);
ConversionUtils.replicateDriverContact(circuit, resetInputPin);
// Convert the gate according to the extended mapping data
GateUtils.convertGate(circuit, component, extendedMapping);
return true;
}

private static BooleanFormula getResetInverterFormula(boolean activeLow, boolean initToOne,
BooleanVariable in1Var, BooleanVariable in2Var) {
private static BooleanFormula getFormulaWithReset(BooleanFormula formula, BooleanVariable initVar,
boolean activeLow, boolean initToOne) {

if (initToOne) {
if (activeLow) {
return new Not(new And(in1Var, in2Var));
if (formula instanceof Not notFormula) {
return new Not(new And(notFormula.getX(), initVar));
} else {
return new Or(formula, new Not(initVar));
}
} else {
return new Not(new And(new Not(in1Var), in2Var));
if (formula instanceof Not notFormula) {
return new Not(new And(notFormula.getX(), new Not(initVar)));
} else {
return new Or(formula, initVar);
}
}
} else {
if (activeLow) {
return new Not(new Or(new Not(in1Var), in2Var));
if (formula instanceof Not notFormula) {
return new Not(new Or(notFormula.getX(), new Not(initVar)));
} else {
return new And(formula, initVar);
}
} else {
return new Not(new Or(in1Var, in2Var));
if (formula instanceof Not notFormula) {
return new Not(new Or(notFormula.getX(), initVar));
} else {
return new And(formula, new Not(initVar));
}
}
}
}

private static Collection<VisualFunctionComponent> resetComponent(VisualCircuit circuit,
private static Collection<VisualFunctionComponent> appendResetToComponent(VisualCircuit circuit,
VisualFunctionComponent component, VisualContact resetPort, boolean isActiveLow) {

return component.isMapped()
Expand Down Expand Up @@ -469,39 +411,13 @@ private static VisualFunctionContact getOrCreateResetPin(VisualCircuit circuit,
private static void insertResetFunction(VisualFunctionContact contact, VisualContact resetContact, boolean activeLow) {
BooleanFormula setFunction = contact.getSetFunction();
BooleanFormula resetFunction = contact.getResetFunction();
Contact resetVar = resetContact.getReferencedComponent();
if (activeLow) {
if (contact.getInitToOne()) {
if (setFunction != null) {
contact.setSetFunction(DUMB_WORKER.or(DUMB_WORKER.not(resetVar), setFunction));
}
if (resetFunction != null) {
contact.setResetFunction(DUMB_WORKER.and(resetVar, resetFunction));
}
} else {
if (setFunction != null) {
contact.setSetFunction(DUMB_WORKER.and(resetVar, setFunction));
}
if (resetFunction != null) {
contact.setResetFunction(DUMB_WORKER.or(DUMB_WORKER.not(resetVar), resetFunction));
}
}
} else {
if (contact.getInitToOne()) {
if (setFunction != null) {
contact.setSetFunction(DUMB_WORKER.or(resetVar, setFunction));
}
if (resetFunction != null) {
contact.setResetFunction(DUMB_WORKER.and(DUMB_WORKER.not(resetVar), resetFunction));
}
} else {
if (setFunction != null) {
contact.setSetFunction(DUMB_WORKER.and(DUMB_WORKER.not(resetVar), setFunction));
}
if (resetFunction != null) {
contact.setResetFunction(DUMB_WORKER.or(resetVar, resetFunction));
}
}
Contact initVar = resetContact.getReferencedComponent();
boolean initToOne = contact.getInitToOne();
if (setFunction != null) {
contact.setSetFunction(getFormulaWithReset(setFunction, initVar, activeLow, initToOne));
}
if (resetFunction != null) {
contact.setResetFunction(getFormulaWithReset(resetFunction, initVar, activeLow, !initToOne));
}
}

Expand Down

0 comments on commit 552a278

Please sign in to comment.