DIRECTORY Collections, IntFunctions, IntStuff, LichenArrayStuff, LichenDataOps, LichenDataStructure, PairCollections, Rope; LichenChecking: CEDAR PROGRAM IMPORTS Collections, LichenArrayStuff, LichenDataOps, LichenDataStructure, PairCollections, Rope EXPORTS LichenDataOps = BEGIN OPEN LichenDataOps, LichenArrayStuff, LichenDataStructure, Colls:Collections, PairColls:PairCollections, Ints:IntStuff, IntFns:IntFunctions; 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"]; {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: 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, 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[]; toCompln: Function--parent StatEdge _ BoolSeq(index_child present)-- ~ PairColls.CreateHashFn[invable: FALSE]; CheckStatEdge: PROC [ra: REF ANY] ~ { se: StatEdge ~ NARROW[ra]; parents: ARRAY BOOL OF Port _ ALL[NIL]; 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].HasPair[[sv.port, se]] THEN ERROR Error["Broken"]; 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]; FOR d: Dim IN Dim DO IF ABS[se.d[d]] > 1 THEN ERROR; ENDLOOP; IF rep > ignore AND parents[FALSE]#NIL AND parents[TRUE]#NIL THEN { size: NATURAL ~ parents[FALSE].lastChild.PortIndex[]+1; IF parents[FALSE]#parents[TRUE] AND size # parents[TRUE].lastChild.PortIndex[]+1 THEN RETURN; {i: NATURAL ~ se.vs[FALSE].port.PortIndex[]; IF i#se.vs[TRUE].port.PortIndex[] THEN RETURN; {pvs: ARRAY BOOL OF StatVertex ~ [ FALSE: NEW [StatVertexPrivate _ [parents[FALSE], se.vs[FALSE].phase]], TRUE: NEW [StatVertexPrivate _ [parents[TRUE], se.vs[TRUE].phase]]]; pse: StatEdge _ FindStatEdge[psr, [pvs, se.d]]; pse2: StatEdge ~ FindStatEdge[sr, [pvs, se.d]]; compln: BoolSeq--index_child present--; IF pse2 # NIL THEN SELECT rep FROM ignore => ERROR; report, check => Fail[rep, rep, "both child (%g) and parent (%g) edges present in static graph", se, pse2]; establish => ERROR nyet--have to rip out this child--; ENDCASE => ERROR; IF pse=NIL THEN { pse _ AddStatEdge[psr, [pvs, se.d]]; toCompln.AddNewPair[[pse, compln _ CreateBoolSeq[size, FALSE]]]} ELSE compln _ NARROW[toCompln.Apply[pse].val]; compln[i] _ TRUE; }}}; RETURN}; CheckParent: PROC [pair: PairColls.Pair] ~ { pse: StatEdge ~ NARROW[pair[left]]; compln: BoolSeq ~ NARROW[pair[right]]; FOR i: NATURAL IN [0 .. compln.length) DO IF NOT compln[i] THEN EXIT; REPEAT FINISHED => SELECT rep FROM ignore => ERROR; report, check => Fail[rep, rep, "Static graph should have higher-level edge %g", pse]; establish => ERROR nyet; ENDCASE => ERROR; ENDLOOP; 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.Enumerate[CheckStatEdge]; FOR b: BOOL IN BOOL DO CheckIndex: PROC [pair: PairColls.Pair] ~ { ep: Port ~ NARROW[pair[left]]; se: StatEdge ~ NARROW[pair[right]]; IF NOT sr.edges.HasMember[se] THEN ERROR Error["Broken"]; IF se.vs[b].port # ep THEN ERROR Error["Broken"]; RETURN}; sr.portEdge[b].Enumerate[CheckIndex]; ENDLOOP; IF rep>ignore THEN toCompln.Enumerate[CheckParent]; RETURN}; CheckWireAgainstPort: PROC [wire: Wire, port: Port, andInsertIn: Set] = { subWire: Wire _ wire.firstChild; subPort: Port _ port.firstChild; [] _ andInsertIn.AddElt[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]; }; CheckComponent: PROC [ci: CellInstance, rep: AssertionOp] = { portsConnected: VarSet = Colls.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.AddElt[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]]; 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.HasMember[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.AddColl[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 [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 Last tweaked by Mike Spreitzer on October 20, 1987 8:11:36 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™A—K˜KšΟk œr˜{K˜šΡbnxœœ˜KšœY˜`Kšœ˜—K˜Kš œœ7ΟnœŸ œŸœ Ÿœ˜’K˜display™™aLšΟmœ  œ œ œ™Lšœ œ œ)™HLš œ œ  œ œ œ  œ œ™I——™™>Lš  œ œ œ  œ œ™LšœΟgœ$™D—™;Lš œ œ œ œ œ œ œ œ™3—™:Lš œ œ œ œ œ œ œ™L™——™0™GLš œ œ œ œ‘œ œ œ œ œ œ œ œ œ™R—™Kšœœ%˜<šœœ˜Kšœœ˜/Kšœœœ˜Kšœœœ˜