DIRECTORY Asserting, GList, IntHashTable, LichenDataStructure, LichenDataOps, LichenSetTheory, Rope;

LichenChecking: CEDAR PROGRAM
IMPORTS Asserting, IntHashTable, LichenDataStructure, LichenDataOps, LichenSetTheory, Rope
EXPORTS LichenDataOps =

BEGIN OPEN LichenDataStructure, LichenDataOps, LichenSetTheory;


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 _ 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"];
{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];
};
EnumerateInstances[ct, PerInstance]};
SELECT norm FROM
ignore => NULL;
report, check => IF OutersToo THEN {
PerPortDatum: PROC [key, value: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
port: Port =  NARROW[key];
pd: PortDatum = NARROW[value];
IF NOT pd.used THEN Fail[normal, norm, "%g fails ANPortUsedO", port];
IF pd.assoc # NIL THEN Fail[normal, norm, "%g fails ANPortsMergedO", port];
};
[] _ portData.Pairs[PerPortDatum];
};
establish => IF OutersToo THEN {
PerPort: PROC [port: Port] = {
pd: PortDatum = NARROW[portData.Fetch[port].value];
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].value 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;
};

FetchFBJoint: PROC [a: Array, d: Dim, foo, bar: INT] RETURNS [j: Joint] = {
j _ NARROW[a.joints[d][bar + foo*a.jointsPeriod[Bar]]];
};

CheckArray: PROC [ct: CellType] = {
a: Array = ct.asArray;
CheckPortConnections: PROC [key, value: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
ap: Port = NARROW[key];
apc: ArrayPortConnections = NARROW[value];
FOR e: End IN End DO FOR d: Dim IN Dim DO
index: ArrayIndex _ ALL[SELECT e FROM low => 0, high => a.size[d]-1, ENDCASE => ERROR];
od: Dim = OtherDim[d];
PerPair: PROC [key: INT, value: REF ANY] RETURNS [quit: BOOL _ FALSE] --IntHashTable.EachPairAction-- = {
ep: Port = NARROW[value];
index[od] _ key;
IF GetArrayPort[a, index, ep] # ap THEN ERROR Error["Broken"];
};
[] _ apc[e][d].Pairs[PerPair];
ENDLOOP ENDLOOP;
};
FOR d: Dim IN Dim DO FOR foo: INT IN [0 .. a.jointsPeriod[Foo]) DO FOR bar: INT IN [0 .. a.jointsPeriod[Bar]) DO
j: Joint = FetchFBJoint[a, d, foo, bar];
nrp: INT _ 0;
CheckTie: PROC [ra: REF ANY] = {
tie: Tie = NARROW[ra];
n, nIncomplete: INT _ 0;
FOR rpl: RoledPortDataList _ tie.ports, rpl.rest WHILE rpl # NIL DO
IF j.toTie[rpl.first.side].Fetch[rpl.first.port].value # tie THEN ERROR Error["Broken"];
n _ n + 1;
ENDLOOP;
IF n # tie.n THEN ERROR Error["Broken"];
IF tie.completion # NIL THEN {
FOR cji: INT IN [0 .. j.size) DO
complete: BOOL = ComputeComplete[j, tie, cji];
IF NOT complete THEN nIncomplete _ nIncomplete + 1;
IF complete # tie.completion[cji] THEN ERROR Error["Broken"];
ENDLOOP;
IF nIncomplete # tie.completion.nIncomplete THEN ERROR Error["Broken"];
};
nrp _ nrp + tie.n;
};
IF j = NIL THEN LOOP;
IF j.size # j.size2[Foo]*j.size2[Bar] THEN ERROR Error["Broken"];
IF j.roles.length # j.nrp OR j.nrp # nrp THEN ERROR Error["Broken"];
[] _ j.ties.Enumerate[CheckTie];
nrp _ 0;
FOR side: End IN End DO
CheckPair: PROC [key, value: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
port: Port = NARROW[key];
tie: Tie = NARROW[value];
IF NOT j.ties.HasMember[tie] THEN ERROR Error["Broken"];
};
[] _ j.toTie[side].Pairs[CheckPair];
nrp _ nrp + j.toTie[side].GetSize[];
IF j.toTie[side].GetSize[] # j.toRole[side].GetSize[] THEN ERROR Error["Broken"];
ENDLOOP;
IF j.nrp # nrp THEN ERROR Error["Broken"];
FOR index: INT IN [0 .. j.roles.length) DO
rpd: RoledPortData = NARROW[j.roles.refs[index]];
IF rpd.index # index OR j.toRole[rpd.side].Fetch[rpd.port].value # rpd THEN ERROR Error["Broken"];
ENDLOOP;
ENDLOOP ENDLOOP ENDLOOP;
[] _ a.portConnections.Pairs[CheckPortConnections];
};

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].value];
ClearSeen: PROC [key, value: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
pd: PortDatum = NARROW[value];
pd.seen_ FALSE;
};
PerNetConnection: PROC [port2: Port, u: Vertex] = {
pd2: PortDatum = NARROW[portData.Fetch[port2].value];
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].value];
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].value];
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, value: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
pd: PortDatum = NARROW[value];
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].value];
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].value];
IF pil.first # surviver THEN {
pd.seen _ TRUE;
};
ENDLOOP;
{InitPortDatum: PROC [port: Port] = {
pd: PortDatum = NARROW[portData.Fetch[port].value];
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].value];
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].value];
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, value: REF ANY] RETURNS [quit: BOOL _ FALSE] -- HashTable.EachPairAction-- = {
port: Port = NARROW[key];
pd: PortDatum = NARROW[value];
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].value];
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, value: 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.
LichenChecking.Mesa
Mike Spreitzer June 22, 1986 7:54:30 pm PDT
When in rep-normal form:
ANHighestBindingRepd: The binding between ports and wires is represented as `highly' as possible.
A n, p [ n f p g n Q p]
(f is effective connectivity, Q is what's obvious in the data structure)
(A ci, p, n [(A i B [0 .. n.length=p.length) n[i] f ci.p[i]) W n f ci.p])
When in circuit-normal form:
ANNetUsed: Each net has a part attached to at least one thing.
A N E n I N, ci, p , ci.p f n
(note that we allow a ci to be m (the world outside this cell type))
ANPortUsedI: Each port is internally attached to something.
A p'' E p' I p'', n, ci, p = p' , p' f n & n f ci.p
ANPortsMergedI: Each net is connected to at most one port.
A n n E p = p' , n f p & n f p'
Implies nets merged.
The following duals are NOT required to be true:
ANPortUsedO: Each port is used for something interesting at least once.
A p'' E p' I p'', p, ci & ci' = m, n , ci.p f n & ci'.p' f n & (ci' = ci V p' = p)
ANPortsMergedO: Each port distinction is used at least once.
A p = p' of ct E ci = m, n, n' , ci.p f n & ci.p' f n' &  n nS 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)
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.
Κ“–

"cedar" style˜
code™K™+—K˜KšΟk	œ[˜dK˜šΡbnxœœ
˜KšœS˜ZKšœ˜K˜Kšœ
œ5˜?K˜
display™™aLšΟm
œ
Ÿ
œŸ
œŸ
œ™Lšœ
Ÿ
œŸ
œ)™HLš
œ
Ÿ
œŸ
œŸ
œŸ
œ
Ÿ
œŸ
œ™I——™™>Lš
Ÿ
œŸ
œŸ
œ
Ÿ
œŸ
œ™LšœΟg
œ$™D—™;LšŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ™3—™:LšŸ
œŸ
œ
Ÿ
œŸ
œŸ
œŸ
œŸ
œ™L™——™0™GLšŸ
œŸ
œŸ
œŸ
œ
 
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œŸ
œ™R—™<LšŸ
œŸ
œ
Ÿ
œŸ
œ
 
œŸ
œŸ
œŸ
œŸ
œŸ
œŸœ™A——™1™KLš
Ϭ
™¨
—™BLš
œ’
™’
——K˜Kšœ
œœ
œ˜K˜Kšœœœ
˜Kšœœœ
˜K˜šΟnœœ
œU˜mš‘œœ˜$Kš
œ)˜)K˜—šœ˜Kšœ
œ
˜Kš
œ0˜0Kšœœ
˜—Kš
œ(˜(K˜—K˜Kšœ
œΟcΠcm
’
œ
˜/Kšœœœ˜'šœœœ˜!Kšœœœ
˜"Kšœœœ
˜Kšœœ˜—K˜š
‘
œœ
œqœœ˜›
K˜šœœ˜)Kš
œ˜Kšœœ
˜Kšœœ
˜—Kšœ	œœ
˜šœ˜Kšœœ
˜Kš
œ
œ
œœœœ
œ
˜GKšœœ
˜—Kš
œœ
œœ
œ9˜mKšœœ˜$Kš
œ˜Kš
œœ
œœ
œ9˜mšœœ˜š‘	œœ˜ šœ
œ
˜˜
Kšœœ
œ
œœœ
œ˜aKšœœ
œ
œœœ
œ˜`K˜—˜Kšœ
œ
œ
œ
œ
œ˜AKšœœ
œ˜-K˜—Kšœœ
˜—Kš
œœœœ
œ˜OK˜—Kš
œ˜K˜—šœœ˜šœ˜Kšœ
œ
˜˜Kšœœ
˜Kš
œ˜K˜—Kšœœ
˜—Kšœœ
œ!œœœ
œ œœ
œ/˜Ώ
šœ
‘œœ˜(Kšœ
œ
œ˜*Kšœ
œ
œ’˜0Kš
œ&˜&K˜—Kš
œ%˜%šœ˜Kšœ
œ
˜šœœœ˜$š‘œœœ
œœœœ’œ˜fKšœœ˜Kšœœ˜Kšœ
œ	œ2˜Ešœœ
œ5˜KK™ 
—K˜—Kš
œ"˜"K˜—šœ
œœ˜ š‘œœ˜Kšœœ˜3Kšœœ
œ
œœ
œ
˜1šœ
œ	œ˜Kšœœ"˜3Kš
œ#˜#Kšœœ
˜Kš
œ.˜.—šœ
œœ
œ˜Kšœœ6˜GKšœœ*˜=Kšœœ
˜Kš
œ/˜/—K˜—K˜K˜—Kšœœ
˜—K˜—šœœœ
œ˜.š‘œœœ
œ˜$Kšœœ˜Kšœœ
œ˜3Kšœœ
œ’œ˜2Kš
œ˜K˜—Kšœœ
œ
œ˜<Kšœ#œ
œ’˜FKšœ+œ
œ˜HKšœIœ˜_Kš
œ;˜;Kš
œ-˜-K˜—Kšœœœ
œ˜6šœœ
œ˜"Kšœ
œ
˜Kšœœœ
œ˜B˜šœ˜(˜Kš
œ˜Kš
œ1˜1K˜—Kšœœœ.˜S—K˜)K˜—Kšœœ
˜—K˜—K˜š‘œœœœ˜KKšœœ-˜7K˜—K˜š‘
œœ˜#K˜š‘œœœ
œœœœ’œ˜nKšœœ˜Kšœœ˜*šœœœ
œœ˜)Kšœœ
œœ œœ˜WK˜š‘œœœ	œ
œœœœ’œ˜iKšœœ˜K˜Kšœ!œ
œ˜>K˜—K˜Kšœ
œ
˜—K˜—šœœœ
œœ
œœ
œœ
œ˜pK˜(Kšœœ˜
š‘œœœ
œ˜ Kšœœ˜Kšœœ˜šœ.œœ
˜CKšœ;œ
œ˜XK˜
Kšœ
˜—Kšœœ
œ˜(šœœ
œ˜šœœ
œ˜ Kšœ
œ ˜.Kšœ
œ
œ˜3Kšœ œ
œ˜=Kšœ
˜—Kšœ*œ
œ˜GK˜—K˜K˜—Kšœœ
œ
œ
˜Kšœ$œ
œ˜AKšœœ
œ
œ˜DK˜ K˜šœœ˜š‘	œœœ
œœœœ’œ˜cKšœ
œ˜Kšœœ˜Kšœ
œœ
œ˜8K˜—K˜$K˜$Kšœ4œ
œ˜QKšœ
˜—Kšœ
œ
œ˜*šœœ
œ˜*Kšœœ˜1Kšœœ0œ
œ˜bKšœ
˜—Kšœ
œ
œ
˜—Kš
œ3˜3K˜—K˜š‘œœ/˜IKš
œ ˜ K˜ Kš
œ&˜&š	œœ
œœ
˜(Kš
œ4˜4K˜K˜Kšœ
˜—Kšœœ
œœ
œ
œ<˜hK˜—K˜š‘
œœB˜UK˜šœ˜Kšœ
œ
˜˜š‘
œœ˜1Kšœœ˜3š‘	œœœ
œœœœ’œ˜cKšœœ˜Kšœ	œ
˜K˜—š‘œœ˜3Kšœœ˜5Kšœœœ
˜Kšœœœœ
˜-K˜—Kš
œ˜Kš
œ5˜5Kšœ
œ	œ
œ2˜Kšœœ˜"š‘
œœ˜"Kšœœ˜5Kšœ
œœœ˜CK˜—Kšœœ
˜K˜#K˜
—šœ˜Kšœœœ
˜š	œœœœ
˜6Kšœœ!˜8šœ
œ
œ˜Kšœ
œ
œœ˜HK˜
—Kšœ˜Kšœ
˜—K˜—Kš
œ˜—Kš
œ0˜0K˜—Kšœœ
˜—K˜—K˜š‘œœ˜.Kšœ
’qœ
˜wK˜—K˜š‘œœXœœ˜
š
‘œœœ!œœ˜NKšœœ˜Kšœœ
˜Kšœ#œ
˜(š‘œœ˜-Kšœœ˜šœœ˜Kš
œ˜Kšœœ˜Kšœœ
˜Kš
œ
˜
—Kšœ+œ˜5K˜—Kš
œ/˜/Kš
œ˜Kšœœ˜4šœœ
œ˜&Kšœ
œ
˜Kš
œB˜B˜Kšœœ#˜4Kšœ
œ
˜Kš
œ&˜&Kšœ'œ
˜4Kšœ!œ
˜&Kš
œ:˜:K˜—Kšœœ
˜—šœ=œœ
˜VKšœ(œ
˜-Kš
œ9˜9Kšœœ
˜#Kšœœ˜&Kšœœ
˜#Kšœ
˜—Kšœœ˜"Kšœœ
˜(šœ˜Kšœ
œ
˜˜Kšœ
œœ-˜BKšœ
œ
œ9˜PK˜—˜šœ
œœ˜Kšœœ˜/Kšœ
œ
˜Kš
œ&˜&Kš
œ˜Kšœ!œ
˜&Kš
œ;˜;—šœ
œ
œ˜Kšœœ)˜:Kšœ
œ
˜Kš
œ&˜&Kš
œ5˜5Kšœ!œ
˜&Kš
œ;˜;—K˜—Kšœœ
˜—K˜—Kšœ
œ
˜Kšœœ
œ
˜Kš
œ
˜
K˜—K˜š‘œœ(˜<K˜&Kšœ	œœ
˜š‘œœ&˜<Kšœ œ
˜$Kšœœœ
˜š‘
œœ˜/Kšœ
œ%œ
œJ˜šœœ
˜š
œ˜Kšœœœœ
œœ+œ	œ
˜}Kš
œ1˜1Kš
œ˜—š
œ˜Kšœœ
˜K˜Kš
œ˜—š
œ˜Kšœa˜fKš
œ˜—Kšœœ
˜—Kš
œ˜—Kšœ;œœ˜\Kšœœ
œ˜$Kš
œœœ
œ	œ
˜=šœœœ
œ˜"Kš
œ(˜(šœ˜Kšœ
œ
˜Kš
œz˜zš
œ˜Kš‘œœ4˜BKšœœO˜`Kšœ0œœ˜HKš
œ>˜>Kšœ
œ
˜K˜—Kšœœ
˜—Kš
œ˜—K˜—š‘œœ˜Kšœ7œ
œ[˜ž
K˜—šœ
˜šœ˜
Kšœœœ
œœœ
œ/˜•
Kšœœœ
œœœ
œ/˜”
K˜—šœ˜	Kšœœ
œœ
œœœ
œN˜Ώ
K˜—Kšœœ
˜—Kš
œ˜Kšœœ˜&K˜ K˜Kšœ	œ˜)K˜—K˜š‘	œœ
œœ˜JKš
˜š‘œœ%˜7Kš
œ˜K˜—š‘œœ%˜2Kšœœœ%˜8Kš
œ˜K˜—Kšœ'œ
œ
˜4Kšœ
œ
œœ˜'Kš
œ˜K˜Kš
œ.˜.šœœ
œ˜ Kšœœ
œ9œ%˜Kš
œ"˜"Kš
œ8˜8Kšœœ
˜Kšœœ
˜K˜—K˜Kš
œD˜DKšœ
˜—K˜š‘
œœœ+˜Zš
‘œœœœœ˜4Kšœ
œœœ
œ
œ˜=—Kšœœ˜ K˜Kš
œ˜Kšœœœ
˜&Kš
œ˜K˜Kš	œ'œ
œ
œœ
˜9Kšœœ˜Kšœœ˜š‘	œœœ
œœœœ’œ˜cKšœœ˜Kšœ	œ
˜K˜—Kšœœ
œ
˜Kšœœœ
œ
’!œ
˜RKšœœ
œ˜5Kš
œ˜š	œœœœ
˜6Kšœœ"˜8Kšœ	œ
œ˜&Kšœ
œ
˜Kšœ
˜—Kšœœ
œ
œ˜-Kš
œ˜š	œœœœ
˜6Kšœœ"˜8šœœ˜Kšœ
œ
˜K˜—Kšœ
˜—šœ
‘
œœ˜%Kšœœ˜3Kšœœ
œ	œ˜8Kšœœ
˜K˜—K˜#šœœ˜š‘œœ#˜5Kšœ
œ˜Kšœœ˜1šœ	œœ˜"Kš
œ˜Kš
œ˜—K˜—Kšœœ=˜KKš
œ?˜?K˜—šœ
‘œœ˜(Kšœœ'˜;š‘œœ#˜5Kšœ
œ˜Kšœœ˜1šœ	œœ˜"Kš
œ˜Kš
œ˜—K˜—Kš
œ)˜)Kš
œ&˜&K˜—K˜%šœœ˜š‘œœœ
œœœœ’œ˜gKšœ
œ˜Kšœœ˜šœ
œ	œ˜Kšœ
œ˜Kšœœ
˜šœ$œœ
˜>Kšœœ'˜>šœ
œ
˜Kšœœ˜/Kšœœœ
˜Kšœœœ˜<Kšœœ˜!—Kšœ
˜—K˜—K˜—Kš
œ"˜"K˜—K˜—K˜š‘
œœ1˜Aš‘œœ˜'Kš
œ˜Kš
œ&˜&K˜—Kšœœ+˜EK˜$Kš
œ˜—K˜š‘œœœ
œœœœ˜KKšœœ˜Kš
œ2˜2—K˜š‘œœ
œ
’œcœœ˜§
š‘œœœ
œ˜Kšœœ˜Kš
œJ˜JK˜—K˜K˜—K˜š
‘œœœ
œœ˜6šœœ˜Kš
œ˜Kš
œ˜Kš
œ˜Kš
œ˜Kšœœ˜——K˜š‘œœœ
œœœ˜0šœœ˜Kšœ
œ
˜Kšœ	œ
˜Kšœœ˜——K˜Kšœœ˜2š‘œœœ
œ˜<Kš
œ˜Kš
œ˜Kš
œ˜—K˜š‘œœ5œœ
œœ˜kKš
œ0˜0šœ˜Kšœ
œ"˜2Kšœ	œ ˜.Kšœœ
˜—K˜—K˜š‘œœœ˜Dš‘
œœ˜$Kšœœ˜,Kš
œ ˜ —Kš
œ˜K˜"K˜—K˜Kšœ
˜——…—Mξo…