DIRECTORY AbSets, BasicTime, BiRels, LichenArrayStuff, LichenDataOps, LichenDataStructure, Process, Rope, SetBasics;

LichenChecking: CEDAR PROGRAM
IMPORTS AbSets, BasicTime, BiRels, LichenArrayStuff, LichenDataOps, LichenDataStructure, Process, Rope, SetBasics
EXPORTS LichenDataOps =

BEGIN OPEN LichenDataOps, LichenArrayStuff, LichenDataStructure, Sets:AbSets;


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;
IF debugging THEN Log["\nAt %g, checking design %g\n", LIST[NEW [Time _ [BasicTime.Now[]]], Describe[design]]];
EnumerateCellTypes[design, PerCellType];
IF debugging THEN Log["At %g, done checking design %g\n", LIST[NEW [Time _ [BasicTime.Now[]]], Describe[design]]];
RETURN};

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;
Process.CheckForAbort[];
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, FALSE];
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];
};
[] _ 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", LIST[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", LIST[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: Sets.Value] = {
ci: CellInstance = NARROW[elt.VA];
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, rep];
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 [act: CellType, rep: AssertionOp] = {
a: Array ~ act.asArray;
sr: StatRep ~ a.statrep;
psr: StatRep ~ CreateStatRep[];
changed: BOOL _ FALSE;
connected: Function--statEdge _ {$TRUEU$FALSEU$MAYBE}-- ~ BiRels.CreateHashFn[spaces: [statEdges, SetBasics.refs], invable: TRUE];
maybes: Set--of StatEdge-- ~ connected.MappingA[$MAYBE, rightToLeft];
connds: Set--of StatEdge-- ~ connected.MappingA[$TRUE, rightToLeft];
Queue: PROC [sep: StatEdgePrivate] RETURNS [parentConnected: BOOL] ~ {
se: StatEdge ~ MakeStatEdge[sep];
SELECT connected.ApplyA[se].MDA FROM
$FALSE => RETURN [FALSE];
$TRUE => RETURN [TRUE];
$MAYBE => RETURN [FALSE];
NIL => {[] _ connected.AddAA[se, $MAYBE]; RETURN CheckUp[se]};
ENDCASE => ERROR;
};
CheckUp: PROC [se: StatEdge] RETURNS [parentConnected: BOOL] ~ {
parents: ARRAY BOOL OF Port _ ALL[NIL];
Check: PROC [b: BOOL] ~ {
sv: StatVertex ~ se.vs[b];
WITH sv.port.parent SELECT FROM
p: Port => IF p#a.eltType.port THEN parents[b] _ p;
ct: CellType => NULL;
ENDCASE => ERROR;
RETURN};
Check[FALSE];
Check[TRUE];
IF parents[FALSE]#NIL AND parents[TRUE]#NIL AND parents[FALSE].lastChild.PortIndex[]=parents[TRUE].lastChild.PortIndex[] THEN RETURN Queue[[
vs: [
FALSE: NEW [StatVertexPrivate _ [parents[FALSE], se.vs[FALSE].phase]],
TRUE: NEW [StatVertexPrivate _ [parents[TRUE], se.vs[TRUE].phase]]],
d: se.d]];
RETURN [FALSE]};
CheckStatEdge: PROC [ra: REF ANY] ~ {
se: StatEdge ~ NARROW[ra];
Check: PROC [b: BOOL] ~ {
sv: StatVertex ~ se.vs[b];
IF sv.port.PortCCT # a.eltType THEN ERROR Error["Broken"];
FOR d: Dim IN Dim DO
IF sv.phase[d] >= a.basePeriod[d] THEN ERROR Error["Broken"];
ENDLOOP;
IF NOT sr.portEdge[b].HasAA[sv.port, se] THEN ERROR Error["Broken"];
RETURN};
Check[FALSE];
Check[TRUE];
FOR d: Dim IN Dim DO
IF ABS[se.d[d]] > 1 THEN ERROR;
ENDLOOP;
IF rep > ignore THEN [] _ CheckUp[se];
RETURN};
EvalEdge: PROC [se: StatEdge] RETURNS [connd: BOOL] ~ {
SELECT connected.ApplyA[se].MDA FROM
$FALSE => RETURN [FALSE];
$TRUE => RETURN [TRUE];
ENDCASE => NULL;
connd _ FindStatEdge[sr, se^]#NIL;
IF (NOT connd) THEN {
childs: ARRAY BOOL OF Port _ [
FALSE: se.vs[FALSE].port.FirstChildPort[],
TRUE: se.vs[TRUE].port.FirstChildPort[]];
connd _ childs[FALSE]#NIL AND childs[TRUE]#NIL;
WHILE connd AND childs[FALSE]#NIL DO
sub: BOOL ~ EvalEdge[MakeStatEdge[[
vs: [
NEW[StatVertexPrivate_ [childs[FALSE],se.vs[FALSE].phase]],
NEW[StatVertexPrivate_ [childs[FALSE],se.vs[FALSE].phase]]],
d: se.d]]];
connd _ sub;
childs[FALSE] _ childs[FALSE].NextChildPort[];
childs[TRUE] _ childs[TRUE].NextChildPort[];
ENDLOOP;
connd _ connd};
[] _ connected.AddAA[se, IF connd THEN $TRUE ELSE $FALSE];
RETURN};
IF a.size # INT[a.size2[Foo]]*a.size2[Bar] THEN ERROR Error["Broken"];
FOR d: Dim IN Dim DO
IF a.basePeriod[d] > a.size2[d] THEN ERROR Error["Broken"];
ENDLOOP;
IF a.buildPhase#statrepFixed THEN ERROR Error["Broken"];
IF sr=NIL OR a.dumrep=NIL THEN ERROR Error["Broken"];
sr.edges.EnumA[CheckStatEdge];
FOR b: BOOL IN BOOL DO
CheckIndex: PROC [left, right: REF ANY] ~ {
ep: Port ~ NARROW[left];
se: StatEdge ~ NARROW[right];
IF NOT sr.edges.HasMemA[se] THEN ERROR Error["Broken"];
IF se.vs[b].port # ep THEN ERROR Error["Broken"];
RETURN};
sr.portEdge[b].EnumAA[CheckIndex];
ENDLOOP;
IF rep>ignore THEN {
CheckDown: PROC [sep: StatEdgePrivate] ~ {
childs: ARRAY BOOL OF Port _ [
FALSE: sep.vs[FALSE].port.FirstChildPort[],
TRUE: sep.vs[TRUE].port.FirstChildPort[]];
WHILE childs[FALSE]#NIL DO
csep: StatEdgePrivate ~ [
vs: [
NEW [StatVertexPrivate _ [childs[FALSE], sep.vs[FALSE].phase]],
NEW [StatVertexPrivate _ [childs[FALSE], sep.vs[FALSE].phase]]],
d: sep.d];
cse: StatEdge ~ FindStatEdge[sr, csep];
IF cse#NIL THEN SELECT rep FROM
report, check => Fail[rep, rep, "Static edge %g redundant with ancestor", cse];
establish => {
IF debugging THEN Log["Removing descendant edge %g.\n", LIST[cse]];
RemStatEdge[sr, cse];
changed _ TRUE};
ENDCASE => ERROR;
CheckDown[csep];
childs[FALSE] _ childs[FALSE].NextChildPort[];
childs[TRUE] _ childs[TRUE].NextChildPort[];
ENDLOOP;
RETURN};
CheckConnd: PROC [val: REF ANY] ~ {
se: StatEdge ~ NARROW[val];
IF CheckUp[se] THEN RETURN;
IF FindStatEdge[sr, se^]=NIL THEN SELECT rep FROM
report, check => Fail[rep, rep, "Effective static edge %g not represented", se];
establish => {
IF debugging THEN Log["Adding ancestor edge %g.\n", LIST[se]];
[] _ AddStatEdge[sr, se^];
changed _ TRUE};
ENDCASE => ERROR;
CheckDown[se^];
RETURN};
WHILE NOT maybes.Empty[] DO
se: StatEdge ~ NARROW[maybes.AnElt[].MA];
[] _ EvalEdge[se];
ENDLOOP;
connds.EnumA[CheckConnd];
rep _ rep};
RETURN};

CheckWireAgainstPort: PROC [wire: Wire, port: Port, andInsertIn: Set] = {
subWire: Wire _ wire.firstChild;
subPort: Port _ port.firstChild;
[] _ andInsertIn.AddA[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};
};
CheckVertex[v];
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", LIST[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", LIST[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", LIST[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];
};

Break: SIGNAL ~ CODE;
break: SteppyName _ NIL;

CheckComponent: PROC [ci: CellInstance, rep: AssertionOp] = {
portsConnected: VarSet = Sets.CreateHashSet[];
altered: BOOL _ FALSE;
CheckConnections: PROC [parent: Port, cellward, v: Vertex] RETURNS [nv: Vertex] ~ {
containingWire, subWire: Wire _ NIL;
first, match: BOOL _ TRUE;
PerConnection: PROC [port: Port, w: Vertex] = {
IF NOT portsConnected.AddA[port] THEN ERROR Error["Broken: Port %g multiply connected on cell instance %g", port, v];
IF port.parent#parent THEN ERROR Error["Broken: edge for port %g out of place", LIST[port]];
IF break#NIL AND w.VertexNames.HasMemA[break] THEN Break;
WITH w SELECT FROM
wire: Wire => NULL;
im: Intermediary => w _ CheckConnections[port, v, im];
ci: CellInstance => NULL;
ENDCASE => ERROR;
WITH w SELECT FROM
wire: Wire => {
IF first THEN {first _ FALSE; subWire _ wire; match _ wire.containingWire#NIL AND wire.containingWire.firstChild=wire}
ELSE IF match AND wire # (subWire _ NextChildWire[subWire]) THEN match _ FALSE;
CheckWireAgainstPort[wire, port, portsConnected];
};
im: Intermediary => match _ first _ FALSE;
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 WITH v SELECT FROM
x: CellInstance => IF IsMirror[x] AND x.type.firstInstance=NIL AND x.type.firstArray=NIL THEN NULL ELSE ERROR Error["Broken"];
x: Wire => ERROR;
x: Intermediary => ERROR Error["Broken"];
ENDCASE => ERROR;
IF match AND (NOT first) AND NextChildWire[subWire] # NIL THEN match _ FALSE;
nv _ v;
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", parent, containingWire];
establish => {
Unlinkem: PROC [port: Port, w: Vertex, e: Edge] = {RemoveEdges[e]};
IF debugging THEN Log["Making connection between port %g and wire %g.\n", LIST[parent, containingWire]];
EnumerateImmediateEdges[v, Unlinkem, [cellward: FALSE, wireward: TRUE]];
AddEdge[[cellward: cellward, wireward: containingWire], parent];
nv _ containingWire;
altered _ TRUE;
};
ENDCASE => ERROR;
};
};
CheckCover: PROC [port: Port] = {
IF portsConnected.HasMemA[port] # (port # ci.type.port) THEN ERROR Error["Broken: Port %g not properly covered by connections to cell instance %g", port, ci];
};
CheckVertex[ci];
SELECT IsMirror[ci] FROM
FALSE => {
IF (IF ci.prevInstance # NIL THEN ci.prevInstance.nextInstance ELSE ci.type.firstInstance) # ci THEN ERROR Error["Broken: Cell type - instance linkage"];
IF (IF ci.nextInstance # NIL THEN ci.nextInstance.prevInstance ELSE ci.type.lastInstance) # ci THEN ERROR Error["Broken: Cell type - instance linkage"];
};
TRUE => {
IF ci.prevInstance # NIL OR ci.nextInstance # NIL OR ci.type.firstInstance = ci OR ci.type.lastInstance = ci THEN ERROR Error["Broken: Mirror %g linked among instances of cell type %g", ci, ci.type];
};
ENDCASE => ERROR;
EnsurePublic[ci.type];
IF ci # CheckConnections[ci.type.port, NIL, ci] THEN ERROR;
EnumeratePorts[ci.type, CheckCover];
IF altered THEN {
PrintOnLog[ci];
CheckComponent[ci, check];
};
RETURN};

CheckVertex: PROC [v: Vertex] ~ {
dir: GraphDirection _ cellward;
e: Edge _ v.firstEdge;
WHILE e#NIL DO
mySide: GraphDirection ~ e.SideFor[v];
curDir: GraphDirection ~ OppositeDirection[mySide];
next: Edge ~ e.sides[mySide].next;
IF e.sides[mySide].v#v THEN ERROR Error["Broken"];
IF curDir#dir THEN SELECT dir FROM
cellward => dir _ wireward;
wireward => ERROR Error["Broken: AI1 violated at vertex %g by edge %g", v, e];
ENDCASE => ERROR;
e _ next;
ENDLOOP;
RETURN};

MergeNets: PUBLIC PROC [net1, net2: Wire] RETURNS [merged, doomed: Wire] = {
MoveToMerged: PROC [port: Port, w: Vertex, e: Edge] = {
IF e.sides[wireward].v#doomed THEN ERROR;
e.sides[wireward].v _ merged;
RETURN};
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 doomed.firstEdge.sides[wireward].v#merged THEN ERROR;
IF merged.lastEdge=NIL THEN merged.firstEdge _ doomed.firstEdge ELSE {
IF merged.lastEdge.sides[wireward].v#merged THEN ERROR;
merged.lastEdge.sides[wireward].next _ doomed.firstEdge};
merged.lastEdge _ doomed.lastEdge;
doomed.firstEdge.sides[wireward].prev _ merged.lastEdge;
doomed.firstEdge _ NIL;
doomed.lastEdge _ NIL;
};
DeleteVertex[doomed];
[] _ merged.VertexNames.AddSet[doomed.VertexNames];
IndexVertexNames[merged, doomed.VertexNames];
RETURN};

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]];
IF siNet=NIL THEN ERROR;
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]}
};
IF soNet=NIL THEN ERROR;
EnumerateImmediateEdges[v, OuterCleanup];
[] _ noteIn.Store[v.containingCT, $T];
};
EnumerateInstances[ct, FixInstance, FALSE]};
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, FALSE];
};

FixAffectedType: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ TRUE] = {
parent: CellType = NARROW[key];
CheckCellType[parent, ignore, establish, ignore]};

CheckCellTypes: PUBLIC PROC [cts: ConstSet--of CellType--, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, interface, internals, instances: BOOL _ TRUE] = {
Checkit: PROC [val: REF ANY] = {
ct: CellType = NARROW[val];
CheckCellType[ct, rep, norm, comparable, interface, internals, instances];
};
cts.EnumA[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
Last tweaked by Mike Spreitzer on January 8, 1988 11:36:51 am PST
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™A—K˜KšÏk	œk˜tK˜šÑbnxœ�œ
�˜Kš�œj˜qKš�œ˜—K˜Kš�œ
�œ7Ïnœ˜MK˜
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˜šŸœ�œ
�œU˜mšŸœ�œ˜$Kš
œ)˜)K˜—š�œ�˜Kšœ
�œ
˜Kš
œ0˜0Kš�œ�œ
˜—Kš�œ�œ&�œ
�œ0˜oKš
œ(˜(Kš�œ�œ)�œ
�œ0˜rKš�œ˜—K˜Kšœ
�œÏcÐcm
¢
œ
˜/Kšœ�œ�œ˜'šœ�œ�œ˜!Kšœ�œ�œ
˜"Kšœ�œ
˜Kšœ�œ˜—K˜š
Ÿ
œ�œ
�œq�œ�œ˜›
K˜šœ�œ�˜)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š�œ
�œ
�œ˜*Kš�œ
�œ
�œ¢˜0Kš
œ&˜&Kš
œ˜K˜—šŸœ�œ˜"K˜Kš
�œ�œ
�œ�œ
�œ˜6Kš
œ˜K˜—Kšœ$�œ˜+Kš
œ˜Kš�œ�œ
�œ˜5Kš
œ˜š�œ�˜Kšœ
�œ
˜šœ�œ�œ˜$šŸœ�œ�œ
�œ�œ�œ�œ¢œ˜dKšœ�œ˜Kšœ�œ˜Kš�œ
�œ	�œ2˜Eš�œ�œ
�œ5˜KK™ 
—K˜—Kš
œ"˜"K˜—šœ
�œ�œ˜ šŸœ�œ˜Kšœ�œ˜1Kš�œ�œ
�œ
�œ�œ
�œ
˜1š�œ
�œ	�œ˜Kš�œ�œ�œ˜9Kš
œ#˜#Kšœ�œ
˜Kš
œ.˜.—š�œ
�œ�œ
�œ˜Kš�œ�œ(�œ˜MKšœ�œ*˜=Kšœ�œ
˜Kš
œ/˜/—K˜—K˜K˜—Kš�œ�œ
˜—K˜—š�œ�œ�œ
�œ˜.šŸœ�œ˜'Kšœ�œ�œ˜"Kš�œ�œ
�œ˜3Kš�œ�œ
�œ¢œ˜2Kš
œ˜K˜—Kš�œ�œ
�œ
�œ˜<Kš�œ#�œ
�œ¢˜FKš�œ+�œ
�œ˜HKš�œI�œ�˜_Kš
œ;˜;Kš
œ-˜-K˜—Kš�œ�œ�œ
�œ˜;š�œ�œ
�œ�˜"Kšœ
�œ
˜Kšœ�œ�œ
�œ˜B˜š�œ�˜&˜Kš
œ˜Kš
œ1˜1K˜—Kš�œ�œ�œ.˜S—K˜)K˜—Kš�œ�œ
˜—K˜—K˜šŸ
œ�œ&˜6K˜Kš
œ˜Kš
œ˜Kšœ	�œ�œ
˜Kšœ¢£
¢£
¢£
¢	œE�œ˜‚
Kšœ¢œ+˜EKšœ¢œ*˜DšŸœ�œ�œ�œ˜FKš
œ!˜!š�œ�œ
�˜$Kšœ
�œ�œ˜Kšœ	�œ�œ˜Kšœ
�œ�œ˜Kš�œ'�œ˜>Kš�œ�œ
˜—Kš
œ˜—šŸœ�œ�œ�œ˜@Kšœ	�œ
�œ
�œ�œ
�œ˜'šŸœ�œ�œ˜Kš
œ˜š�œ�œ
�˜Kšœ�œ�œ˜3Kšœ�œ
˜Kš�œ�œ
˜—Kš�œ˜—Kšœ�œ˜
Kšœ�œ˜š�œ	�œ�œ
�œ	�œ�œ
�œ	�œ �œ�œ
�œ˜Œ
š
œ˜Kš�œ�œ�œ	�œ
˜FKš�œ�œ�œ	�œ˜D—Kš¡
œ¡
œ˜
—Kš�œ�œ˜—šŸ
œ�œ�œ
�œ˜%Kšœ�œ˜šŸœ�œ�œ˜Kš
œ˜Kš�œ�œ
�œ˜:š�œ�œ�˜Kš�œ �œ
�œ˜=Kš�œ
˜—Kš�œ
�œ#�œ
�œ˜DKš�œ˜—Kšœ�œ˜
Kšœ�œ˜š�œ�œ�˜Kš
�œ
�œ¡
œ	�œ
�œ
˜Kš�œ
˜—Kš�œ�œ˜&Kš�œ˜—šŸœ�œ�œ	�œ˜7š�œ�œ
�˜$Kšœ
�œ�œ˜Kšœ	�œ�œ˜Kš�œ�œ
˜—Kšœ�œ
˜"š�œ�œ�œ˜šœ�œ
�œ
�œ	˜Kš�œ�œ˜*Kš�œ�œ˜)—Kšœ�œ�œ
�œ�œ�œ
˜/š	�œ�œ�œ�œ
�˜$šœ�œ˜#˜Kš�œ�œ�œ
˜;Kš�œ�œ�œ˜<—K˜—Kš
œ˜Kšœ�œ�œ˜.Kšœ�œ�œ˜,Kš�œ
˜—Kš
œ˜—Kšœ�œ�œ�œ	˜:Kš�œ˜—Kš�œ
�œ�œ
�œ˜Fš�œ�œ�˜Kš�œ�œ
�œ˜;Kš�œ
˜—Kš�œ�œ
�œ˜8Kš�œ�œ
�œ
�œ
�œ
�œ˜5Kš
œ˜š	�œ�œ
�œ
�œ
�˜šŸ
œ�œ�œ
�œ˜+Kšœ�œ˜Kšœ�œ˜Kš�œ
�œ�œ
�œ˜7Kš�œ�œ
�œ˜1Kš�œ˜—Kš
œ"˜"Kš�œ
˜—š�œ�œ˜šŸ	œ�œ˜*šœ�œ
�œ
�œ	˜Kš�œ	�œ˜+Kš�œ	�œ˜*—š�œ�œ�œ
�˜š
œ˜š
œ˜Kš�œ�œ
�œ
˜?Kš�œ�œ
�œ˜@—Kš¡
œ¡
œ˜
—Kš
œ'˜'š	�œ�œ
�œ
�œ�˜Kš
œO˜Oš
œ˜Kš�œ�œ'�œ˜CKš
œ˜Kšœ
�œ˜—Kš�œ�œ
˜—Kš
œ˜Kšœ�œ�œ˜.Kšœ�œ�œ˜,Kš�œ
˜—Kš�œ˜—šŸ
œ�œ�œ
�œ˜#Kšœ�œ˜Kš�œ
�œ
�œ
˜š	�œ�œ
�œ
�œ�˜1Kš
œP˜Pš
œ˜Kš�œ�œ#�œ˜>Kš
œ˜Kšœ
�œ˜—Kš�œ�œ
˜—K˜Kš�œ˜—š�œ
�œ�˜Kšœ�œ�œ˜)K˜Kš�œ
˜—Kš
œ˜K˜—Kš�œ˜—K˜šŸœ�œ/˜IKš
œ ˜ K˜ Kš
œ˜š	�œ�œ
�œ�œ
�˜(Kš
œ4˜4K˜K˜Kš�œ
˜—Kš�œ�œ
�œ�œ
�œ
�œ<˜hK˜—K˜šŸ
œ�œB˜UK˜š�œ�˜Kšœ
�œ
˜˜šŸ
œ�œ˜1Kšœ�œ˜1šŸ	œ�œ�œ
�œ�œ�œ�œ¢œ˜aKšœ�œ˜Kšœ	�œ
˜K˜—šŸœ�œ˜3Kšœ�œ˜3Kš�œ�œ�œ
˜Kš�œ�œ�œ�œ
˜-K˜—Kš
œ˜Kš
œ5˜5Kš�œ
�œ	�œ
�œ2˜Kš�œ�œ˜"šŸ
œ�œ˜"Kšœ�œ˜3Kš�œ
�œ�œ�œ˜CK˜—Kšœ�œ
˜K˜#K˜
—š�œ˜Kšœ�œ
˜š�œ"�œ�œ
�˜6Kšœ�œ˜6š�œ
�œ
�œ˜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š
œ˜Kšœ�œ˜4š�œ�œ
�œ�˜&Kšœ
�œ
˜Kš
œB˜B˜Kš�œ�œ�œ	˜:Kšœ
�œ
˜Kš
œ&˜&Kšœ'�œ
˜4Kšœ!�œ
˜&Kš
œ:˜:K˜—Kš�œ�œ
˜—š�œ=�œ�œ
�˜VKšœ(�œ
˜-Kš
œ9˜9Kšœ�œ
˜#Kšœ�œ˜&Kšœ�œ
˜#Kš�œ
˜—Kšœ�œ˜"Kšœ�œ
˜(š�œ�˜Kšœ
�œ
˜˜Kš�œ
�œ�œ-˜BKš�œ
�œ
�œ9˜PK˜—˜š�œ
�œ�œ˜Kš�œ�œ�œ˜5Kšœ
�œ
˜Kš
œ&˜&Kš
œ˜Kšœ!�œ
˜&Kš
œ;˜;—š�œ
�œ
�œ˜Kš�œ�œ�œ˜@Kšœ
�œ
˜Kš
œ&˜&Kš
œ5˜5Kšœ!�œ
˜&Kš
œ;˜;—K˜—Kš�œ�œ
˜—K˜—Kšœ
�œ
˜Kš�œ�œ
�œ
˜Kš
œ
˜
K˜—K˜KšŸœ�œ�œ
˜Kšœ�œ
˜K˜šŸœ�œ)˜=K˜.Kšœ	�œ�œ
˜šŸœ�œ%�œ¡
œ˜SKšœ �œ
˜$Kšœ�œ�œ
˜šŸ
œ�œ˜/Kš�œ
�œ�œ
�œJ˜uKš�œ�œ
�œ0�œ˜\Kš�œ�œ
�œ�œ˜9š�œ�œ
�˜Kšœ�œ
˜Kš
œ6˜6Kšœ�œ
˜Kš�œ�œ
˜—š�œ�œ
�˜š
œ˜Kš
�œ�œ
�œ.�œ
�œ%˜vKš
�œ
�œ�œ+�œ	�œ
˜OKš
œ1˜1Kš
œ˜—Kšœ$�œ
˜*š
œ˜Kš�œa˜fKš
œ˜—Kš�œ�œ
˜—Kš
œ˜—Kšœ;�œ�œ˜\š	�œ�œ
�œ�œ
�˜ Kšœ�œ
�œ�œ
�œ�œ
�œ
�œ
�œ
�œ˜~Kšœ�œ
˜Kšœ�œ˜)Kš�œ�œ
˜—Kš�œ�œ�œ�œ�œ
�œ	�œ
˜MKš¡
œ˜š�œ�œ�œ
�œ˜"Kš
œ(˜(š�œ�˜Kšœ
�œ
˜Kš
œ|˜|š
œ˜KšŸœ�œ5˜CKš�œ�œ9�œ˜hKšœ0�œ�œ˜HKš
œ@˜@Kš¡
œ˜Kšœ
�œ
˜K˜—Kš�œ�œ
˜—Kš
œ˜—K˜—šŸ
œ�œ˜!Kš�œ6�œ
�œ\˜ž
K˜—K˜š�œ�˜š�œ˜
Kš�œ�œ�œ
�œ�œ�œ
�œ/˜™
Kš�œ�œ�œ
�œ�œ�œ
�œ/˜˜
K˜—š�œ˜	Kš�œ�œ
�œ�œ
�œ�œ�œ
�œP˜Ç
K˜—Kš�œ�œ
˜—Kš
œ˜Kš�œ%�œ�œ
�œ
˜;K˜$š�œ	�œ˜Kš
œ˜Kš
œ˜K˜—Kš�œ˜—K˜šŸœ�œ˜!Kš
œ˜K˜š�œ�œ
�˜Kš
œ&˜&Kš
œ3˜3K˜"Kš�œ�œ
�œ˜2š�œ�œ
�œ�˜"Kš
œ˜Kšœ�œ=˜NKš�œ�œ
˜—K˜	Kš�œ
˜—Kš�œ˜—K˜šŸ	œ�œ
�œ�œ˜LšŸœ�œ%˜7Kš�œ�œ
�œ
˜)Kš
œ˜Kš�œ˜—Kš�œ'�œ
�œ
˜4Kš�œ
�œ
�œ�œ˜'Kš
œ˜K˜Kš
œ.˜.š�œ�œ
�œ˜ Kš�œ+�œ
�œ
˜8š�œ�œ
�œ%�œ˜FKš�œ*�œ
�œ
˜7Kš
œ9˜9—Kš
œ"˜"Kš
œ8˜8Kšœ�œ
˜Kšœ�œ
˜K˜—K˜K˜3K˜-Kš�œ˜—K˜šŸ
œ�œJ˜ZšŸœ�œ�œ�œ˜4Kšœ
�œ�œ�œ
�œ
�œ˜=—Kšœ�œ˜ K˜Kš
œ˜Kšœ�œ�œ
˜&Kš
œ˜K˜Kš	œ'�œ
�œ
�œ�œ
˜9Kšœ�œ˜Kšœ�œ˜šŸ	œ�œ�œ
�œ�œ�œ�œ¢œ˜aKšœ�œ˜Kšœ	�œ
˜K˜—Kš�œ�œ
�œ
˜Kš�œ�œ�œ
�œ
�¢!œ
˜RKš�œ�œ
�œ˜5Kš
œ˜š�œ!�œ�œ
�˜6Kšœ�œ ˜6Kš�œ	�œ
�œ˜&Kšœ
�œ
˜Kš�œ
˜—Kš�œ�œ
�œ
�œ˜-Kš
œ˜š�œ!�œ�œ
�˜6Kšœ�œ ˜6š�œ�œ˜Kšœ
�œ
˜K˜—Kš�œ
˜—šœ
Ÿ
œ�œ˜%Kšœ�œ˜1Kš�œ�œ
�œ	�œ˜8Kš�œ�œ
˜K˜—K˜#š�œ�œ˜šŸœ�œ#˜5Kšœ
�œ˜Kšœ�œ˜/š�œ	�œ�œ˜"Kš
œ˜Kš
œ˜—K˜—Kšœ�œ=˜KKš�œ�œ
�œ
�œ
˜Kš
œ?˜?K˜—šœ
Ÿœ�œ˜(Kšœ�œ'˜;šŸœ�œ#˜5Kšœ
�œ˜Kšœ�œ˜/š�œ	�œ�œ˜"Kš
œ˜Kš
œ˜—K˜—Kš�œ�œ
�œ
�œ
˜Kš
œ)˜)Kš
œ&˜&K˜—Kšœ$�œ˜,š�œ�œ˜šŸœ�œ�œ
�œ�œ�œ�œ¢œ˜eKšœ
�œ˜Kšœ�œ˜š�œ
�œ	�œ˜Kš
œ˜Kšœ�œ
˜š�œ$�œ�œ
�˜>Kšœ�œ%˜<š�œ
�œ
�˜Kšœ�œ˜/Kšœ�œ�œ
˜Kšœ�œ�œ˜<Kš�œ�œ˜!—Kš�œ
˜—K˜—K˜—Kš
œ"˜"K˜—K˜—K˜šŸ
œ�œ1˜AšŸœ�œ˜'Kš
œ˜Kš
œ&˜&K˜—Kš�œ�œ+˜EKšœ$�œ˜+Kš
œ˜—K˜šŸœ�œ�œ
�œ�œ�œ�œ˜IKšœ�œ˜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š�œ
˜—…—]T…m