LichenChecking:
CEDAR
PROGRAM
IMPORTS Asserting, LichenArrayStuff, LichenDataOps, LichenDataStructure, LichenSetTheory, Rope
EXPORTS LichenDataOps =
BEGIN OPEN LichenSetTheory, LichenDataOps, LichenArrayStuff, LichenDataStructure;
When in rep-normal form:
ANHighestBindingRepd: The binding between ports and wires is represented as `highly' as possible.
n, p [ n é p Ò n Ä p]
(é is effective connectivity, Ä is what's obvious in the data structure)
( ci, p, n [( i [0 .. n.length=p.length) n[i] é ci.p[i]) { n é ci.p])
When in circuit-normal form:
ANNetUsed: Each net has a part attached to at least one thing.
N n † N, ci, p ci.p é n
(note that we allow a ci to be m (the world outside this cell type))
ANPortUsedI: Each port is internally attached to something.
p'' p' † p'', n, ci, p ` p' p' é n ' n é ci.p
ANPortsMergedI: Each net is connected to at most one port.
n ¬ p ` p' n é p & n é p'
Implies nets merged.
The following duals are NOT required to be true:
ANPortUsedO: Each port is used for something interesting at least once.
p'' p' † p'', p, ci & ci' ` m, n ci.p é n ' ci'.p' é n ' (ci' ` ci ( p' ` p)
ANPortsMergedO: Each port distinction is used at least once.
p ` p' of ct ci ` m, n, n' ci.p é n ' ci.p' é n' ' n ¬H n'
For a design to be comparable, we must also have:
ACCellTypeEquivd: The structural equivalence class of a cell type is clear.
ct.equivClass # implicitClass COR |ct.names.designed| = 1 OR |ct.names.designed| = 0 CAND (|ct.names.unknown| = 1 OR |ct.names.unknown| = 0 CAND |ct.names.progged| = 1)
ACPortEquivd: The structural equivalence class of a port is clear.
p.equivClass # implicitClass COR |p.names.designed| = 1 OR |p.names.designed| = 0 CAND (|p.names.unknown| = 1 OR |p.names.unknown| = 0 CAND |p.names.progged| = 1)
PortList: TYPE = LIST OF Port;
debugging: BOOL ← TRUE;
OutersToo: BOOL = FALSE;
CheckDesign:
PUBLIC
PROC [design: Design, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp] = {
PerCellType:
PROC [ct: CellType] = {
CheckCellType[ct, rep, norm, comparable];
};
SELECT norm
FROM
ignore => NULL;
report, check, establish => EnsureAllIn[design];
ENDCASE => ERROR;
EnumerateCellTypes[design, PerCellType];
};
PortData: TYPE = RefTable--port b port datum--;
PortDatum: TYPE = REF PortDatumPrivate;
PortDatumPrivate:
TYPE =
RECORD [
used, seen, deleted: BOOL ← FALSE,
assoc: PortList ← NIL,
newPort: Port ← NIL];
CheckCellType:
PUBLIC
PROC [ct: CellType, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, interface, internals, instances:
BOOL ←
TRUE] = {
portData: PortData;
consequences: RefTable =
SELECT norm
FROM
establish => CreateRefTable[],
ignore, report, check => NIL,
ENDCASE => ERROR;
altered: BOOL ← FALSE;
SELECT norm
FROM
ignore, report, check => NULL;
establish => IF NOT (interface AND internals AND instances) THEN ERROR;
ENDCASE => ERROR;
IF ct.privateKnown AND NOT ct.publicKnown THEN ERROR Error["Broken: private parts known but not the public"];
IF internals THEN EnsurePrivate[ct];
EnsurePublic[ct];
IF ct.privateKnown AND NOT ct.publicKnown THEN ERROR Error["Broken: private parts known but not the public"];
IF interface
THEN {
CheckPort:
PROC [port: Port] = {
WITH port.parent
SELECT
FROM
pp: Port => {
IF (IF port.prev # NIL THEN port.prev.next ELSE pp.firstChild) # port THEN ERROR Error["Broken"];
IF (IF port.next # NIL THEN port.next.prev ELSE pp.lastChild) # port THEN ERROR Error["Broken"];
};
ct: CellType => {
IF port.next # NIL OR port.prev # NIL THEN ERROR Error["Broken"];
IF ct.port # port THEN ERROR Error["Broken"];
};
ENDCASE => ERROR;
IF (port.firstChild # NIL) # (port.lastChild # NIL) THEN ERROR Error["Broken"];
};
EnumeratePorts[ct, CheckPort];
};
IF instances
THEN {
SELECT norm
FROM
ignore => NULL;
report, check, establish => {
ct.wasntNormalized ← FALSE;
portData ← CreatePortData[ct];
};
ENDCASE => ERROR;
IF (ct.firstInstance # NIL AND ct.firstInstance.prevInstance # NIL) OR (ct.lastInstance # NIL AND ct.lastInstance.nextInstance # NIL) THEN ERROR Error["Broken: cell type - instance linkage"];
{useCount: INT ← 0;
PerInstance:
PROC [v: CellInstance] = {
IF v.type # ct THEN ERROR Error["Broken"];
IF IsMirror[v] THEN ERROR Error["Broken"]; --AM2
CheckInstance[v, portData, rep, norm];
useCount ← useCount + 1;
};
PerArray:
PROC [act: CellType] = {
a: Array = act.asArray;
IF a=NIL OR a.eltType # ct THEN ERROR Error["Broken"];
useCount ← useCount + 1;
};
EnumerateInstances[ct, PerInstance];
EnumerateArrays[ct, PerArray];
IF useCount # ct.useCount THEN ERROR Error["Broken"];
};
SELECT norm
FROM
ignore => NULL;
report, check =>
IF OutersToo
THEN {
PerPortDatum:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
FALSE]
--HashTable.EachPairAction-- = {
port: Port = NARROW[key];
pd: PortDatum = NARROW[val];
IF NOT pd.used THEN Fail[normal, norm, "%g fails ANPortUsedO", port];
IF pd.assoc #
NIL
THEN Fail[normal, norm, "%g fails ANPortsMergedO", port];
Note that we depend on ANPortsMergedO being true for some other cellTypes, and ANPortsMergedI being true for this and some other cellTypes, in making this test.
};
[] ← portData.Pairs[PerPortDatum];
};
establish =>
IF OutersToo
THEN {
PerPort:
PROC [port: Port] = {
pd: PortDatum = NARROW[portData.Fetch[port].val];
IF (NOT pd.used) AND (pd.assoc # NIL) THEN ERROR;
IF
NOT pd.used
THEN {
IF debugging THEN Log["Deleting port %g.\n", port];
DeletePort[ct, port, consequences];
ct.wasntNormalized ← TRUE;
CheckCellType[ct, ignore, ignore, comparable]}
ELSE
IF pd.assoc #
NIL
THEN {
IF debugging THEN Log["On Type %g, merging ports %g.\n", ct, pd.assoc];
MergePorts[ct, CONS[port, pd.assoc], portData, consequences];
ct.wasntNormalized ← TRUE;
CheckCellType[ct, ignore, ignore, comparable]};
};
EnumeratePorts[ct, PerPort];
};
ENDCASE => ERROR;
};
IF internals
AND ct.asUnorganized #
NIL
THEN {
PerInstance:
PROC [elt:
REF
ANY] = {
ci: CellInstance = NARROW[elt];
IF ci.containingCT # ct THEN ERROR Error["Broken"];
IF IsMirror[ci] THEN ERROR Error["Broken"]--AM1--;
CheckComponent[ci, rep];
};
IF ct.asUnorganized.mirror = NIL THEN ERROR Error["Broken"];
IF ct.asUnorganized.mirror.type # ct THEN ERROR Error["Broken"]; --AM3
IF ct.asUnorganized.mirror.containingCT # ct THEN ERROR Error["Broken"];
IF CheckNet[ct.asUnorganized.internalWire, norm, comparable, consequences] THEN altered ← TRUE;
ct.asUnorganized.containedInstances.Enumerate[PerInstance];
CheckComponent[ct.asUnorganized.mirror, rep];
};
IF internals AND ct.asArray # NIL THEN CheckArray[ct];
IF instances
THEN
SELECT norm
FROM
ignore => NULL;
report, check => IF ct.wasntNormalized THEN ERROR Error["Broken"];
establish => {
SELECT consequences.Fetch[ct].val
FROM
$T => {
[] ← consequences.Delete[ct];
CheckCellType[ct, ignore, establish, comparable];
};
ENDCASE => IF ct.wasntNormalized THEN CheckCellType[ct, ignore, check, comparable];
[] ← consequences.Pairs[FixAffectedType];
};
ENDCASE => ERROR;
};
CheckArray:
PROC [ct: CellType] = {
a: Array = ct.asArray;
FOR d: Dim
IN Dim
DO
gp: GroupingParms = a.groupingParmses[d];
hasMiddle: BOOL = gp.middle.maxPlusOne > gp.middle.min;
peculiar: INT = gp.middle.min + a.size[d] - gp.middle.maxPlusOne;
nMid: NAT = IF hasMiddle THEN a.jointsPeriod[d] ELSE 0;
firstHigh: INT = gp.middle.min + nMid;
IF
gp.middle.min < 0 OR
gp.middle.maxPlusOne > a.size[d] OR
gp.middle.maxPlusOne < gp.middle.min OR
gp.firstHigh # firstHigh OR
gp.sum # peculiar + nMid OR
gp.d # firstHigh - gp.middle.maxPlusOne
THEN ERROR Error["Broken"];
IF a.nextRP[d] # a.roles[d].length THEN ERROR Error["Broken"];
FOR index:
NAT
IN [0 .. a.roles[d].length)
DO
rpd: SidedPortData = NARROW[a.roles[d].refs[index]];
IF rpd #
NIL
AND (
rpd.index # index OR
a.toRole[d][rpd.side].Fetch[rpd.port].val # rpd OR
(index#0 AND rpd.links = NIL AND RPDNeedsLinks[a, d, rpd]))
THEN ERROR Error["Broken"];
ENDLOOP;
FOR side: End
IN End
DO
CheckToRole:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
FALSE]
--HashTable.EachPairAction-- = {
port: Port = NARROW[key];
rpd: SidedPortData = NARROW[val];
IF rpd.side # side OR rpd.port # port OR rpd.index >= a.nextRP[d] THEN ERROR Error["Broken"];
};
IF a.toRole[d][side].Pairs[CheckToRole] THEN ERROR;
ENDLOOP;
FOR
f
f:
INT
IN [0 .. a.jointsPeriod[Foo])
DO
FOR
f
b:
INT
IN [0 .. a.jointsPeriod[Bar])
DO
phase: Nat2 = [ff, fb];
j: Joint = GetArrayJoint[a, d, phase];
rawLair: Range2 =
IF d = Foo
THEN [[0, a.size[Foo]-1], [0, a.size[Bar]-0]]
ELSE [[0, a.size[Foo]-0], [0, a.size[Bar]-1]];
jiir: Range2 = Range2Div[r: rawLair, t: a.jointsPeriod, f: phase];
size2: Size2 = RangeShape[jiir];
middle: Range2 = Range2Div[r: [a.groupingParmses[Foo].middle, a.groupingParmses[Bar].middle], t: a.jointsPeriod, f: phase];
IF jiir[Foo].min # 0 OR jiir[Bar].min # 0 THEN ERROR;
IF
j = NIL OR
j.size # j.size2[Foo]*j.size2[Bar] OR
j.size2 # size2
THEN ERROR Error["Broken"];
FOR dc: Dim
IN Dim
DO
IF
j.groupingParmses[dc].middle # middle[dc]
THEN ERROR Error["Broken"];
ENDLOOP;
ENDLOOP ENDLOOP;
ENDLOOP;
};
CheckWireAgainstPort:
PROC [wire: Wire, port: Port, andInsertIn: Set] = {
subWire: Wire ← wire.firstChild;
subPort: Port ← port.firstChild;
[] ← andInsertIn.UnionSingleton[port];
WHILE subWire #
NIL
AND subPort #
NIL
DO
CheckWireAgainstPort[subWire, subPort, andInsertIn];
subWire ← subWire.next;
subPort ← subPort.next;
ENDLOOP;
IF subWire # NIL OR subPort # NIL THEN ERROR Error["Broken: Wire %g doesn't match port %g", wire, port];
};
CheckInstance:
PROC [v: CellInstance, portData: PortData, rep, norm: AssertionOp] = {
CheckComponent[v, rep];
SELECT norm
FROM
ignore => NULL;
report, check, establish => {
PerConnection:
PROC [port: Port, net: Vertex] = {
pd: PortDatum = NARROW[portData.Fetch[port].val];
ClearSeen:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
FALSE]
--HashTable.EachPairAction-- = {
pd: PortDatum = NARROW[val];
pd.seen← FALSE;
};
PerNetConnection:
PROC [port2: Port, u: Vertex] = {
pd2: PortDatum = NARROW[portData.Fetch[port2].val];
IF u = v THEN pd2.seen ← TRUE;
IF u # v OR port2 # port THEN pd.used ← TRUE;
};
[] ← portData.Pairs[ClearSeen];
EnumerateImmediateConnections[net, PerNetConnection];
IF NOT pd.seen THEN ERROR Error["Broken: Port %g half connected to", port];
IF v = v.type.firstInstance
THEN {
StartAssoc:
PROC [port2: Port] = {
pd2: PortDatum = NARROW[portData.Fetch[port2].val];
IF pd2.seen AND port # port2 THEN pd.assoc ← CONS[port2, pd.assoc];
};
pd.assoc ← NIL;
EnumeratePorts[v.type, StartAssoc];
}
ELSE {
lastAssoc: PortList ← NIL;
FOR la: PortList ← pd.assoc, la.rest
WHILE la #
NIL
DO
pd2: PortDatum = NARROW[portData.Fetch[la.first].val];
IF
NOT pd2.seen
THEN {
IF lastAssoc = NIL THEN pd.assoc ← la.rest ELSE lastAssoc.rest ← la.rest
}
ELSE lastAssoc ← la;
ENDLOOP;
};
};
EnumerateImmediateConnections[v, PerConnection];
};
ENDCASE => ERROR;
};
CheckIntermediate:
PROC [im: Intermediary] = {
NULL --er, nothing to do here, since the intermediates are checked as part of the cell instance checking, uh, right?--;
};
CheckNet:
PROC [v: Wire, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, noteIn: RefTable]
RETURNS [altered:
BOOL] = {
Work:
PROC [v: Wire]
RETURNS [portSeen, otherSeen, portUsed:
BOOL ←
FALSE] = {
portCount, otherCount: NAT ← 0;
ports: PortList ← NIL;
iAmPorted, anNetUsed, anPortUsedI: BOOL;
SeekPortage:
PROC [port: Port, w: Vertex] = {
ci: CellInstance = NARROW[w];
IF IsMirror[ci]
THEN {
portCount ← portCount + 1;
ports ← CONS[port, ports];
portSeen ← TRUE;
}
ELSE {otherCount ← otherCount + 1; otherSeen ← TRUE};
};
EnumerateTransitiveConnections[v, SeekPortage];
iAmPorted ← portSeen;
portUsed ← iAmPorted AND portCount + otherCount > 1;
IF portCount > 1
THEN
SELECT norm
FROM
ignore => ERROR;
report, check => Fail[normal, norm, "%g fails ANPortsMergedI", v];
establish => {
IF debugging THEN Log["Merging ports %g.\n", ports];
altered ← TRUE;
[] ← noteIn.Store[v.containingCT, $T];
[] ← MergePorts[v.containingCT, ports, NIL, noteIn];
v.containingCT.wasntNormalized ← TRUE;
CheckCellType[v.containingCT, ignore, ignore, comparable];
};
ENDCASE => ERROR;
FOR subWire: Wire ← v.FirstChildWire[], subWire.NextChildWire[]
WHILE subWire #
NIL
DO
subPortSeen, subOtherSeen, subPortUsed: BOOL;
[subPortSeen, subOtherSeen, subPortUsed] ← Work[subWire];
portSeen ← portSeen OR subPortSeen;
otherSeen ← otherSeen OR subOtherSeen;
portUsed ← portUsed OR subPortUsed;
ENDLOOP;
anNetUsed ← portSeen OR otherSeen;
anPortUsedI ← portCount = 0 OR portUsed;
SELECT norm
FROM
ignore => ERROR;
report, check => {
IF NOT anNetUsed THEN Fail[normal, norm, "%g fails ANNetUsed", v];
IF NOT anPortUsedI THEN Fail[normal, norm, "%g fails ANPortUsedI", ports.first];
};
establish => {
IF
NOT anNetUsed
THEN {
IF debugging THEN Log["Deleting net %g.\n", v];
altered ← TRUE;
[] ← noteIn.Store[v.containingCT, $T];
DeleteVertex[v];
v.containingCT.wasntNormalized ← TRUE;
CheckCellType[v.containingCT, ignore, ignore, comparable]};
IF
NOT anPortUsedI
THEN {
IF debugging THEN Log["Deleting port %g.\n", ports.first];
altered ← TRUE;
[] ← noteIn.Store[v.containingCT, $T];
[] ← DeletePort[v.containingCT, ports.first, noteIn];
v.containingCT.wasntNormalized ← TRUE;
CheckCellType[v.containingCT, ignore, ignore, comparable]};
};
ENDCASE => ERROR;
};
altered ← FALSE;
IF norm = ignore THEN RETURN;
[] ← Work[v];
};
CheckComponent:
PROC [v: CellInstance, rep: AssertionOp] = {
portsConnected: Set = CreateHashSet[];
altered: BOOL ← FALSE;
CheckConnections:
PROC [port: Port, cellward, v: Vertex] = {
containingWire, subWire: Wire ← NIL;
first, match: BOOL ← TRUE;
PerConnection:
PROC [port: Port, w: Vertex] = {
IF NOT portsConnected.UnionSingleton[port] THEN ERROR Error["Broken: Port %g multiply connected on cell instance %g", port, v];
WITH w
SELECT
FROM
wire: Wire => {
IF first THEN {subWire ← wire; first ← FALSE} ELSE IF match AND wire # (subWire ← NextChildWire[subWire]) THEN match ← FALSE;
CheckWireAgainstPort[wire, port, portsConnected];
};
im: Intermediary => {
match ← first ← FALSE;
CheckConnections[port, v, im];
};
ci: CellInstance => {
ERROR Error["Broken: Found cell instance %g on wireward end of an edge from cell instance %g", ci, v];
};
ENDCASE => ERROR;
};
EnumerateImmediateConnections[v, PerConnection, [cellward: FALSE, wireward: TRUE], forward];
IF first THEN ERROR Error["Broken"];
IF match AND NextChildWire[subWire] # NIL THEN match ← FALSE;
IF match
AND cellward #
NIL
THEN {
containingWire ← subWire.containingWire;
SELECT rep
FROM
ignore => NULL;
report, check => Fail[rep, rep, "Effective connection between port %g and wire %g not represented", port, containingWire];
establish => {
Unlinkem: PROC [port: Port, w: Vertex, e: Edge] = {RemoveEdge[e]};
IF debugging THEN Log["Making connection between port %g and wire %g.\n", port, containingWire];
EnumerateImmediateEdges[v, Unlinkem, [cellward: FALSE, wireward: TRUE]];
AddEdge[[cellward: cellward, wireward: containingWire], port];
altered ← TRUE;
};
ENDCASE => ERROR;
};
};
PerPort:
PROC [port: Port] = {
IF portsConnected.HasMember[port] # (port # v.type.port) THEN ERROR Error["Broken: Port %g not properly covered by connections to cell instance %g", port, v];
};
SELECT IsMirror[v]
FROM
FALSE => {
IF (IF v.prevInstance # NIL THEN v.prevInstance.nextInstance ELSE v.type.firstInstance) # v THEN ERROR Error["Broken: Cell type - instance linkage"];
IF (IF v.nextInstance # NIL THEN v.nextInstance.prevInstance ELSE v.type.lastInstance) # v THEN ERROR Error["Broken: Cell type - instance linkage"];
};
TRUE => {
IF v.prevInstance # NIL OR v.nextInstance # NIL OR v.type.firstInstance = v OR v.type.lastInstance = v THEN ERROR Error["Broken: Mirror %g linked among instances of cell type %g", v, v.type];
};
ENDCASE => ERROR;
EnsurePublic[v.type];
CheckConnections[v.type.port, NIL, v];
EnumeratePorts[v.type, PerPort];
portsConnected.DestroySet[];
IF altered THEN CheckComponent[v, check];
};
MergeNets:
PUBLIC
PROC [net1, net2: Wire]
RETURNS [merged, doomed: Wire] =
BEGIN
MoveToMerged:
PROC [port: Port, w: Vertex, e: Edge] = {
e.sides[wireward].v ← merged;
};
PerName:
PROC [assertion: Asserting.Assertion] = {
name: ROPE = NARROW[Asserting.TermsOf[assertion].first];
KnowVertexName[merged, name];
};
IF net1.containingCT # net2.containingCT THEN ERROR;
IF net1 = net2 THEN RETURN [net1, NIL];
merged ← net1;
doomed ← net2;
EnumerateImmediateEdges[doomed, MoveToMerged];
IF doomed.firstEdge #
NIL
THEN {
IF merged.lastEdge # NIL THEN merged.lastEdge.sides[wireward].next ← doomed.firstEdge ELSE merged.firstEdge ← doomed.firstEdge;
merged.lastEdge ← doomed.lastEdge;
doomed.firstEdge.sides[wireward].prev ← merged.lastEdge;
doomed.firstEdge ← NIL;
doomed.lastEdge ← NIL;
};
DeleteVertex[doomed];
Asserting.EnumerateAssertionsAbout[nameReln, doomed.other, PerName];
END;
MergePorts:
PROC [ct: CellType, ports:
PortList, portData: PortData, noteIn: RefTable] = {
Length:
PROC [ln:
PortList]
RETURNS [len:
NAT ← 0] =
{FOR ln ← ln, ln.rest WHILE ln # NIL DO len ← len+1 ENDLOOP};
numIndices: NAT = Length[ports];
oldPorts: Port = ct.port;
newPorts: Port = oldPorts;
updatePortData: BOOL = portData # NIL;
surviver: Port = ports.first;
siNet: Wire;
designed, unked, progged, recent, old: LIST OF NAT ← NIL;
oldest: INTEGER ← 0;
newPI: NAT ← 0;
ClearSeen:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
FALSE]
--HashTable.EachPairAction-- = {
pd: PortDatum = NARROW[val];
pd.seen← FALSE;
};
IF numIndices < 2 THEN ERROR;
IF numIndices >= 2 AND portData # NIL THEN ERROR--code below might exhibit bugs--;
IF portData = NIL THEN portData ← CreatePortData[ct];
[] ← portData.Pairs[ClearSeen];
FOR pil:
PortList ← ports, pil.rest
WHILE pil #
NIL
DO
pd: PortDatum = NARROW[portData.Fetch[pil.first].val];
IF pd.seen THEN ERROR Error["Broken"];
pd.seen ← TRUE;
ENDLOOP;
IF surviver = NIL THEN ERROR Error["Broken"];
[] ← portData.Pairs[ClearSeen];
FOR pil:
PortList ← ports, pil.rest
WHILE pil #
NIL
DO
pd: PortDatum = NARROW[portData.Fetch[pil.first].val];
IF pil.first # surviver
THEN {
pd.seen ← TRUE;
};
ENDLOOP;
{
InitPortDatum:
PROC [port: Port] = {
pd: PortDatum = NARROW[portData.Fetch[port].val];
IF port = surviver OR NOT pd.seen THEN pd.newPort ← port
ELSE pd.newPort ← NIL;
};
EnumeratePorts[ct, InitPortDatum]};
IF ExpansionKnown[ct]
THEN {
InnerCleanup:
PROC [ip: Port, w: Vertex, e: Edge] = {
iNet: Wire = NARROW[w];
pd: PortDatum = NARROW[portData.Fetch[ip].val];
IF pd.seen
AND iNet # siNet
THEN {
RemoveEdge[e];
[] ← MergeNets[siNet, iNet]}
};
siNet ← NARROW[FindImmediateConnection[ct.asUnorganized.mirror, surviver]];
EnumerateImmediateEdges[ct.asUnorganized.mirror, InnerCleanup];
};
{
FixInstance:
PROC [v: CellInstance] = {
soNet: Wire = NARROW[FindImmediateConnection[v, surviver]];
OuterCleanup:
PROC [op: Port, w: Vertex, e: Edge] = {
oNet: Wire = NARROW[w];
pd: PortDatum = NARROW[portData.Fetch[op].val];
IF pd.seen
AND oNet # soNet
THEN {
RemoveEdge[e];
[] ← MergeNets[soNet, oNet]}
};
EnumerateImmediateEdges[v, OuterCleanup];
[] ← noteIn.Store[v.containingCT, $T];
};
EnumerateInstances[ct, FixInstance]};
IF updatePortData
THEN {
FixPortDatum:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
FALSE]
-- HashTable.EachPairAction-- = {
port: Port = NARROW[key];
pd: PortDatum = NARROW[val];
IF
NOT pd.seen
THEN {
oldAssoc: PortList ← pd.assoc;
pd.assoc ← NIL;
FOR oldAssoc ← oldAssoc, oldAssoc.rest
WHILE oldAssoc #
NIL
DO
pd2: PortDatum = NARROW[portData.Fetch[oldAssoc.first].val];
SELECT
TRUE
FROM
oldAssoc.first = port => ERROR Error["Broken"];
pd2.newPort = NIL => NULL;
pd2.newPort # NIL => pd.assoc ← CONS[pd2.newPort, pd.assoc];
ENDCASE => ERROR Error["Broken"];
ENDLOOP;
};
};
[] ← portData.Pairs[FixPortDatum];
};
};
DeletePort:
PROC [ct: CellType, port: Port, noteIn: RefTable] = {
FixInstance:
PROC [v: CellInstance] = {
UnlinkPort[v, port];
[] ← noteIn.Store[v.containingCT, $T];
};
IF ExpansionKnown[ct] THEN UnlinkPort[ct.asUnorganized.mirror, port];
EnumerateInstances[ct, FixInstance];
};
FixAffectedType:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
TRUE] = {
parent: CellType = NARROW[key];
CheckCellType[parent, ignore, establish, ignore]};
CheckCellTypes:
PUBLIC
PROC [cts: Set
--of CellType--, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, interface, internals, instances:
BOOL ←
TRUE] = {
Checkit:
PROC [ra:
REF
ANY] = {
ct: CellType = NARROW[ra];
CheckCellType[ct, rep, norm, comparable, interface, internals, instances];
};
cts.Enumerate[Checkit];
};
ToAO:
PROC [ra:
REF
ANY]
RETURNS [ao: AssertionOp] = {
ao ←
SELECT ra
FROM
$ignore => ignore,
$report => report,
$check => check,
$establish => establish,
ENDCASE => ERROR};
ToBOOL:
PROC [ra:
REF
ANY]
RETURNS [b:
BOOL] = {
b ←
SELECT ra
FROM
$FALSE => FALSE,
$TRUE => TRUE,
ENDCASE => ERROR};
AssertionFamily: TYPE = {rep, normal, comparable};
AssertionFamilyComplaints:
ARRAY AssertionFamily
OF
ROPE = [
rep: "RepNotNormal: ",
normal: "NotNormal: ",
comparable: "NotComparable: "];
Fail:
PROC [af: AssertionFamily, ao: FailableAssertionOp, msg:
ROPE, v1, v2, v3, v4, v5:
REF
ANY ←
NIL] = {
msg ← AssertionFamilyComplaints[af].Concat[msg];
SELECT ao
FROM
report => SIGNAL Warning[msg, v1, v2, v3, v4, v5];
check => ERROR Error[msg, v1, v2, v3, v4, v5];
ENDCASE => ERROR;
};
CreatePortData:
PROC [ct: CellType]
RETURNS [portData: PortData] = {
InitPortDatum:
PROC [port: Port] = {
pd: PortDatum = NEW [PortDatumPrivate ← []];
[] ← portData.Insert[port, pd]};
portData ← CreateRefTable[];
EnumeratePorts[ct, InitPortDatum];
};
END.