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—™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šœœœ˜