DIRECTORY LichenArrayStuff, Collections, LichenDataOps, LichenDataStructure, IntFunctions, IntStuff, PairCollections, Rope; LichenChecking: CEDAR PROGRAM IMPORTS LichenArrayStuff, Collections, LichenDataOps, LichenDataStructure, 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]; IF instances THEN SELECT norm FROM ignore => NULL; report, check => IF ct.wasntNormalized THEN ERROR Error["Broken"]; establish => { SELECT consequences.Fetch[ct].val FROM $T => { [] _ consequences.Delete[ct]; CheckCellType[ct, ignore, establish, comparable]; }; ENDCASE => IF ct.wasntNormalized THEN CheckCellType[ct, ignore, check, comparable]; [] _ consequences.Pairs[FixAffectedType]; }; ENDCASE => ERROR; }; CheckArray: PROC [ct: CellType] = { a: Array = ct.asArray; middlea: Range2 = GPMiddle[a.groupingParmses]; FOR d: Dim IN Dim DO shaved: Range2 ~ ShaveRange2Top1[middlea, d]; gp: GroupingParms = a.groupingParmses[d]; hasMiddle: BOOL = gp.middle.maxPlusOne > gp.middle.min; peculiar: INT = gp.middle.min + a.size[d] - gp.middle.maxPlusOne; nMid: NAT = IF hasMiddle THEN a.jointsPeriod[d] ELSE 0; firstHigh: INT = gp.middle.min + nMid; IF gp.middle.min < 0 OR gp.middle.maxPlusOne > a.size[d] OR gp.middle.maxPlusOne < gp.middle.min OR gp.firstHigh # firstHigh OR gp.sum # peculiar + nMid OR gp.d # firstHigh - gp.middle.maxPlusOne THEN ERROR Error["Broken"]; IF a.nextRP[d] # a.roles[d].length THEN ERROR Error["Broken"]; FOR index: NAT IN [0 .. a.roles[d].length) DO rpd: SidedPortData = NARROW[a.roles[d].refs[index]]; IF rpd # NIL AND ( rpd.index # index OR a.toRole[d][rpd.side].Fetch[rpd.port].val # rpd OR (index#0 AND rpd.links = NIL AND RPDNeedsLinks[a, d, rpd])) THEN ERROR Error["Broken"]; ENDLOOP; FOR side: End IN End DO CheckToRole: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = { port: Port = NARROW[key]; rpd: SidedPortData = NARROW[val]; IF rpd.side # side OR rpd.port # port OR rpd.index >= a.nextRP[d] THEN ERROR Error["Broken"]; }; IF a.toRole[d][side].Pairs[CheckToRole] THEN ERROR; ENDLOOP; FOR ff: INT IN [0 .. a.jointsPeriod[Foo]) DO FOR fb: INT IN [0 .. a.jointsPeriod[Bar]) DO phase: Nat2 = [ff, fb]; j: Joint = GetArrayJoint[a, d, phase]; rawLair: Range2 = IF d = Foo THEN [[0, a.size[Foo]-1], [0, a.size[Bar]-0]] ELSE [[0, a.size[Foo]-0], [0, a.size[Bar]-1]]; jiir: Range2 = Range2Div[r: rawLair, t: a.jointsPeriod, f: phase]; size2: Size2 = RangeShape[jiir]; middlej: Range2 = Range2Div[r: shaved, t: a.jointsPeriod, f: phase]; IF jiir[Foo].min # 0 OR jiir[Bar].min # 0 THEN ERROR; IF j = NIL OR j.size # j.size2[Foo]*j.size2[Bar] OR j.size2 # size2 THEN ERROR Error["Broken"]; FOR dc: Dim IN Dim DO IF j.groupingParmses[dc].middle # middlej[dc] THEN ERROR Error["Broken"]; ENDLOOP; ENDLOOP ENDLOOP; ENDLOOP; }; CheckWireAgainstPort: PROC [wire: Wire, port: Port, andInsertIn: Set] = { subWire: Wire _ wire.firstChild; subPort: Port _ port.firstChild; [] _ andInsertIn.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 [v: CellInstance, rep: AssertionOp] = { portsConnected: VarSet = Colls.CreateHashSet[]; altered: BOOL _ FALSE; CheckConnections: PROC [parent: Port, cellward, v: 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 => { 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 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; 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]; 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]; }; CheckVertex[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]; IF altered THEN { PrintOnLog[v]; CheckComponent[v, check]; }; }; 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 August 27, 1987 10:04:36 am 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šœH˜OKšœ˜—K˜Kš œœ7ΟnœŸ œŸœ Ÿœ˜’K˜display™™aLšΟmœ  œ œ œ™Lšœ œ œ)™HLš œ œ  œ œ œ  œ œ™I——™™>Lš  œ œ œ  œ œ™LšœΟgœ$™D—™;Lš œ œ œ œ œ œ œ œ™3—™:Lš œ œ œ œ œ œ œ™L™——™0™GLš œ œ œ œ‘œ œ œ œ œ œ œ œ œ™R—™šœœœ˜-Kšœœ˜4šœœœ˜Kšœ˜Kšœ0˜2Kšœ œ œœ˜;—Kšœœ˜Kšœ˜—šœ œ˜šŸ œœ œœœœœ’œ˜cKšœ œ˜Kšœœ˜!Kš œœœœœ˜]K˜—Kšœ&œœ˜3Kšœ˜—šœ‘€œœœœœ‘€œœœ˜YKšœ‘€œ‘€œ˜Kšœ&˜&šœœ˜Kšœ)˜-Kšœ*˜.—Kšœ%‘œ‘œ ˜BK˜ Kšœ€œ ‘œ‘œ ˜DKšœœœœ˜5š˜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šœœœœJ˜wKšœœœ0œ˜\šœœ˜šœ˜Kšœœœœœœ+œ œ˜}Kšœ1˜1Kšœ˜—šœ˜Kšœœ˜K˜Kšœ˜—šœ˜Kšœa˜fKšœ˜—Kšœœ˜—Kšœ˜—Kšœ;œ œ ˜\š œœœœ˜ Kšœœ œœœœœœœœ˜~Kšœ œ˜Kšœœ˜)Kšœœ˜—Kšœœœœœœ œ˜Mšœœ œœ˜"Kšœ(˜(šœ˜Kšœ œ˜Kšœ|˜|šœ˜KšŸœœ5˜CKšœ œ9œ˜hKšœ0œ œ˜HKšœ@˜@Kšœ œ˜K˜—Kšœœ˜—Kšœ˜—K˜—šŸœœ˜Kšœ7œœ[˜žK˜—K˜šœ ˜šœ˜ Kšœœœœœœœ/˜•Kšœœœœœœœ/˜”K˜—šœ˜ KšœœœœœœœœN˜Ώ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˜4K˜-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šœœœ˜