DIRECTORY AbSets, BiRels, LichenDataOps, LichenDataStructure, LichenIntBasics, Process, SetBasics; LichenChecking: CEDAR PROGRAM IMPORTS AbSets, BiRels, LichenDataStructure, LichenIntBasics, Process, SetBasics EXPORTS LichenDataOps = BEGIN OPEN LichenIntBasics, LichenDataOps, LichenDataStructure, Sets:AbSets; CheckDesign: PUBLIC PROC [d: Design] = { CheckSubscript: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { pw: PW ~ pair[left].VA; class: PWClass ~ ClassOfPart[pw]; cct: CellType ~ NARROW[d.cct[class].ApplyA[pw].MA]; kids: Seq--of PW-- ~ BiRels.VB[pair[right]]; CheckKid: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { index: INT ~ pair[left].VI; kid: PW ~ pair[right].VA; IF class # ClassOfPart[kid] THEN Error["Broken"]; IF d.cct[class].ApplyA[kid].MA # cct THEN Error["Broken"]; IF NOT d.parent.HasAA[kid, pw] THEN Error["Broken"]; RETURN [FALSE]}; IF kids.Scan[CheckKid].found THEN ERROR; RETURN [FALSE]}; CheckParent: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { kid: Sets.Value ~ pair[left]; parent: Sets.Value ~ pair[right]; kids: Seq--of PW-- ~ BiRels.VB[d.sub.Apply[parent].Val]; IF NOT kids.HasMapping[kid, rightToLeft] THEN Error["Broken"]; RETURN [FALSE]}; CheckCIType: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { ci: CellInstance ~ NARROW[pair[left].VA]; ct: CellType ~ NARROW[pair[right].VA]; IF NOT (d.cellTypes.HasMemA[ct] AND d.partses[i].HasMemA[ci]) THEN ERROR Error["Broken"]; RETURN [FALSE]}; CheckCTName: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { ct: CellType ~ NARROW[pair[left].VA]; name: ROPE ~ NARROW[pair[right].VA]; IF NOT d.cellTypes.HasMemA[ct] THEN ERROR Error["Broken"]; RETURN [FALSE]}; CheckArrayElt: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { act: CellType ~ NARROW[pair[left].VA]; ect: CellType ~ NARROW[pair[left].VA]; IF NOT (d.cellTypes.HasMemA[act] AND d.cellTypes.HasMemA[ect]) THEN ERROR Error["Broken"]; IF act.asArray=NIL OR d.labelCellTypes.HasMemA[ect] THEN ERROR Error["Broken"]; RETURN [FALSE]}; CheckCIXfm: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { ci: CellInstance ~ NARROW[pair[left].VA]; xfm: Transform ~ VXfm[pair[right]]; IF NOT d.partses[i].HasMemA[ci] THEN ERROR Error["Broken"]; RETURN [FALSE]}; PerCellType: PROC [ctv: Sets.Value] RETURNS [BOOL] = { ct: CellType ~ NARROW[ctv.VA]; IF ct.d # d THEN Error["Broken"]; CheckCellType[ct]; RETURN [FALSE]}; IF d.physd # (d.ciXfm#nilBiRel) OR d.physd # (d.scale#0.0) THEN ERROR Error["Broken"]; IF NOT d.labelCellTypes.Subset[d.cellTypes] THEN ERROR Error["Broken"]; IF NOT d.crossedCellTypes.Subset[d.cellTypes] THEN ERROR Error["Broken"]; IF d.sub.Scan[CheckSubscript].found THEN ERROR; Process.CheckForAbort[]; IF d.parent.Scan[CheckParent].found THEN ERROR; Process.CheckForAbort[]; FOR pc: PartClass IN PartClass DO CheckCCT: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { part: Part ~ NARROW[pair[left].VA]; cct: CellType ~ NARROW[pair[right].VA]; IF ClassOfPart[part]#pc OR NOT d.cellTypes.HasMemA[cct] THEN ERROR Error["Broken"]; IF pc=i THEN { IF NOT d.ciType.HasMapping[pair[left]] THEN ERROR Error["Broken"]; IF d.physd AND NOT d.ciXfm.HasMapping[pair[left]] THEN ERROR Error["Broken"]}; RETURN [FALSE]}; IF d.cct[pc].Scan[CheckCCT].found THEN ERROR; Process.CheckForAbort[]; ENDLOOP; IF d.ciType.Scan[CheckCIType].found THEN ERROR; Process.CheckForAbort[]; IF d.ctName.Scan[CheckCTName].found THEN ERROR; Process.CheckForAbort[]; IF d.arrayElt.Scan[CheckArrayElt].found THEN ERROR; Process.CheckForAbort[]; IF d.physd AND d.ciXfm.Scan[CheckCIXfm].found THEN ERROR; Process.CheckForAbort[]; IF d.cellTypes.Scan[PerCellType].found THEN ERROR; Process.CheckForAbort[]; RETURN}; CheckCellType: PROC [ct: CellType] = { d: Design ~ ct.d; unorg: BOOL ~ ct.asu # NIL; isarray: BOOL ~ ct.asArray # NIL; IF NOT d.cellTypes.HasMemA[ct] THEN Error["Broken"]; IF (ct.asArray#NIL) # d.arrayElt.HasMapA[ct] THEN Error["Broken"]; IF d.physd # (ct.bbox # fullRange2) THEN Error["Broken"]; FOR pc: PartClass IN PartClass DO CheckFullName: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { part: Part ~ pair[left].VA; IF NOT d.cct[pc].HasAA[part, ct] THEN ERROR; RETURN [FALSE]}; IF (ct.fullName[pc]#nilBiRel) # (pc=p OR unorg) THEN Error["Broken"]; IF ct.fullName[pc]#nilBiRel AND ct.fullName[pc].Scan[CheckFullName].found THEN ERROR; Process.CheckForAbort[]; ENDLOOP; IF unorg THEN { CheckConns: PROC [c: Cell, conns: Fn--port _ Wire--, ports: Set--of Port--] ~ { CheckCConn: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { p: Port ~ NARROW[pair[left].VA]; w: Wire ~ NARROW[pair[right].VA]; IF NOT w.conns.HasAA[p, c] THEN ERROR; RETURN [FALSE]}; IF ports.ScanIntersection[LIST[d.isAtomic, conns.SetOn[left].Negate]].found THEN Error["Broken"]; IF conns.Scan[CheckCConn].found THEN ERROR; RETURN}; CheckSubcell: PROC [ra: REF ANY] ~ { ci: CellInstance ~ NARROW[ra]; ict: CellType ~ d.CiT[ci]; IF d.physd THEN { xfm: Transform ~ VXfm[d.ciXfm.ApplyA[ci].Val]; ibb: Range2 ~ TransOffRange2[xfm, ci.offset, ict.bbox]; IF NOT Range2Included[ibb, ct.bbox] THEN Error["Broken"]} ELSE IF ci.offset # dullInt2 THEN Error["Broken"]; CheckConns[ci, ci.conns, ict.CTParts[p]]; RETURN}; CheckWire: PROC [wv: Sets.Value] RETURNS [BOOL] ~ { w: Wire ~ NARROW[wv.VA]; CheckWConn: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { p: Port ~ NARROW[pair[left].VA]; WITH pair[right].VA SELECT FROM ci: CellInstance => IF NOT ci.conns.HasAA[p, w] THEN Error["Broken"]; t: CellType => {IF t#ct THEN Error["Broken"]; IF NOT ct.asu.exports.HasAA[p, w] THEN Error["Broken"]}; ENDCASE => ERROR; RETURN [FALSE]}; IF w.conns.Scan[CheckWConn].found THEN ERROR; RETURN [FALSE]}; ct.Subcells.EnumA[CheckSubcell]; Process.CheckForAbort[]; IF ct.CTParts[w].Scan[CheckWire].found THEN ERROR; Process.CheckForAbort[]; CheckConns[ct, ct.asu.exports, ct.CTParts[p]]; Process.CheckForAbort[]; }; IF isarray THEN { a: Array ~ ct.asArray; sr: StatRep ~ a.statrep; dr: DumRep ~ a.dumrep; ect: CellType ~ ct.EltType; arrayPorts: Set ~ ct.CTParts[p]; eltPorts: Set ~ ect.CTParts[p]; phaseRange: Range2 ~ SizeRange[a.basePeriod]; aiRange: Range2 ~ SizeRange[a.size2]; CheckStatEdge: PROC [sev: Sets.Value] RETURNS [BOOL] ~ { se: StatEdge ~ NARROW[sev.VA]; svA: StatVertex ~ se.SeRSv[sr, FALSE]; svB: StatVertex ~ se.SeRSv[sr, TRUE]; IF NOT (sr.portEdge[FALSE].HasAA[svA.port, se] AND sr.portEdge[TRUE].HasAA[svB.port, se]) THEN Error["Broken"]; IF NOT InRange[svA.phase, phaseRange] THEN Error["Broken"]; IF svB.phase # AddMod[svA.phase, se.d, a.basePeriod] THEN Error["Broken"]; RETURN [FALSE]}; CheckExport: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { ap: Port ~ NARROW[pair[left].VA]; pai: PortAtIndex ~ VPai[pair[right]]; IF NOT (arrayPorts.HasMemA[ap] AND eltPorts.HasMemA[pai.port]) THEN Error["Broken"]; IF NOT InRange[pai.ai, aiRange] THEN Error["Broken"]; RETURN [FALSE]}; CheckDumbWire: PROC [dwv: Sets.Value] RETURNS [BOOL] ~ { dw: DumbWire ~ NARROW[dwv.VA]; CheckEps: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { ep: Port ~ NARROW[pair[left].VA]; cai: CompositeArrayIndex ~ pair[right].VI; dws: Fn ~ BiRels.VB[dr.epToWire.ApplyA[ep].Val]; IF cai >= a.size THEN ERROR; IF NOT dws.HasIA[cai, dw] THEN Error["Broken"]; RETURN [FALSE]}; IF dw.eps.Scan[CheckEps].found THEN ERROR; RETURN [FALSE]}; CheckDWS: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { ep: Port ~ NARROW[pair[left].VA]; dws: Fn ~ BiRels.VB[pair[right]]; CheckIndex: PROC [pair: BiRels.Pair] RETURNS [BOOL] ~ { cai: CompositeArrayIndex ~ pair[left].VI; dw: DumbWire ~ NARROW[pair[right].VA]; IF NOT dw.eps.HasPair[[AV[ep], IV[cai]]] THEN Error["Broken"]; RETURN [FALSE]}; IF dws.SetOn[right].Difference[dr.wires].NonEmpty THEN Error["Broken"]; IF dws.Scan[CheckIndex].found THEN ERROR; RETURN [FALSE]}; IF a.size # Area[a.size2] THEN Error["Broken"]; FOR dim: Dim2 IN Dim2 DO IF a.basePeriod[dim] > a.size2[dim] THEN Error["Broken"]; ENDLOOP; IF d.physd # (a.fXfm#nilBiRel) OR (a.fXfm#nilBiRel) # (a.offsets#NIL) THEN Error["Broken"]; IF a.buildPhase=statrepFixed AND a.dumrep=NIL THEN Error["Broken"]; IF sr.edges.Scan[CheckStatEdge].found THEN ERROR; Process.CheckForAbort[]; FOR b: BOOL IN BOOL DO IF sr.portEdge[b].SetOn[left].Difference[eltPorts].NonEmpty THEN Error["Broken"]; IF NOT sr.portEdge[b].SetOn[right].Equal[sr.edges] THEN Error["Broken"]; IF NOT sr.svEdge[b].SetOn[right].Equal[sr.edges] THEN Error["Broken"]; ENDLOOP; IF sr.apToPAI.Scan[CheckExport].found THEN ERROR; Process.CheckForAbort[]; IF a.buildPhase = statrepFixed THEN { IF dr.epToWire.SetOn[left].Difference[eltPorts].NonEmpty THEN Error["Broken"]; IF dr.apToWire.SetOn[left].Difference[arrayPorts].NonEmpty THEN Error["Broken"]; IF dr.apToWire.SetOn[right].Difference[dr.wires].NonEmpty THEN Error["Broken"]; IF dr.wires.Scan[CheckDumbWire].found THEN ERROR; IF dr.epToWire.Scan[CheckDWS].found THEN ERROR; }; }; RETURN}; END. XLichenChecking.Mesa Last tweaked by Mike Spreitzer on May 7, 1989 12:55:46 pm PDT Κ ϋ– "cedar" style˜code™K™=—K˜KšΟk œY˜bK˜šΡbnxœœ˜KšœI˜PKšœ˜Kšœ˜—K˜Kšœœ6Οnœ˜LK˜šŸ œœœ˜(šŸœœœœ˜;Kšœœœ˜K˜!Kšœœœ˜3Kšœ Οc œ œ˜,šŸœœœœ˜5Kšœœœ˜Kšœœœ˜Kšœœ˜1Kšœœœ˜:Kšœœœ˜4Kšœœ˜—Kšœœœ˜(Kšœœ˜—šŸ œœœœ˜8Kšœ˜Kšœ!˜!Kšœ   œ œ˜8Kšœœ#œ˜>Kšœœ˜—šŸ œœœœ˜8Kšœœ œ˜)Kšœœ œ˜&Kš œœœœœ˜YKšœœ˜—šŸ œœœœ˜8Kšœœ œ˜%Kšœœœ œ˜$Kšœœœœ˜:Kšœœ˜—šŸ œœœœ˜:Kšœœ œ˜&Kšœœ œ˜&Kš œœœœœ˜ZKš œ œœœœ˜OKšœœ˜—šŸ œœœœ˜7Kšœœ œ˜)K˜#Kšœœœœ˜;Kšœœ˜—šŸ œœœœ˜6Kšœœœ˜Kšœ œ˜!Kšœ˜Kšœœ˜—Kšœœœœ˜VKšœœ&œœ˜GKšœœ(œœ˜IKšœ"œœ˜/Kšœ˜Kšœ"œœ˜/Kšœ˜šœœ ˜!šŸœœœœ˜5Kšœ œ œ˜#Kšœœ œ˜'Kš œœœœœ˜Sšœœ˜Kšœœ!œœ˜BKš œ œœ œœ˜N—Kšœœ˜—Kšœ œœ˜-Kšœ˜Kšœ˜—Kšœ"œœ˜/Kšœ˜Kšœ"œœ˜/Kšœ˜Kšœ&œœ˜3Kšœ˜Kšœ œ œœ˜9Kšœ˜Kšœ%œœ˜2Kšœ˜Kšœ˜—K˜šŸ œœ˜&K˜Kšœœ œ˜Kšœ œœ˜!Kšœœœ˜4Kšœ œœ˜BKšœ"œ˜9šœœ ˜!šŸ œœœœ˜:Kšœœ˜Kšœœœœ˜,Kšœœ˜—Kšœ$œœ˜EKšœœ+œœ˜UKšœ˜Kšœ˜—šœœ˜š Ÿ œœ Πcm œ   œ˜OšŸ œœœœ˜7Kšœ œ œ˜ Kšœ œ œ˜!Kšœœœœ˜&Kšœœ˜—Kšœœ.œ˜aKšœœœ˜+Kšœ˜—šŸ œœœœ˜$Kšœœ˜Kšœ˜šœ œ˜Kšœ.˜.Kšœ7˜7Kšœœœ˜9—Kšœœœ˜2Kšœ)˜)Kšœ˜—šŸ œœœœ˜3Kšœ œœ˜šŸ œœœœ˜7Kšœ œ œ˜ šœ œœ˜Kšœœœœ˜EKš œœœœœœ˜fKšœœ˜—Kšœœ˜—Kšœ œœ˜-Kšœœ˜—Kšœ ˜ Kšœ˜Kšœ%œœ˜2Kšœ˜Kšœ.˜.Kšœ˜K˜—šœ œ˜K˜K˜K˜K˜K˜ K˜K˜-K˜%šŸ œœœœ˜8Kšœœœ˜Kšœœ˜&Kšœœ˜%Kš œœœœ œœ˜oKšœœ œ˜;Kšœ"Οgœœ˜JKšœœ˜—šŸ œœœœ˜8Kšœ œ œ˜!Kšœ%˜%Kšœœœœ˜TKšœœœ˜5Kšœœ˜—šŸ œœœœ˜8Kšœœœ˜šŸœœœœ˜5Kšœ œ œ˜!Kšœ'œ˜*Kšœœ˜0Kšœœœ˜Kšœœœ˜/Kšœœ˜—Kšœœœ˜*Kšœœ˜—šŸœœœœ˜5Kšœ œ œ˜!Kšœœ˜!šŸ œœœœ˜7Kšœ&œ˜)Kšœœ œ˜&Kš œœœœœ˜>Kšœœ˜—Kšœ0œ˜GKšœœœ˜)Kšœœ˜—Kšœœ˜/šœ œ˜Kšœ"œ˜9Kšœ˜—Kš œ’œœ’œœœ˜[Kšœœ œœ˜CKšœ$œœ˜1Kšœ˜š œœœœ˜Kšœ:œ˜QKšœœ-œ˜HKšœœ+œ˜FKšœ˜—Kšœ$œœ˜1Kšœ˜šœœ˜%Kšœ7œ˜NKšœ9œ˜PKšœ8œ˜OKšœ$œœ˜1Kšœ"œœ˜/K˜—K˜—Kšœ˜—K˜Kšœ˜—…—".g