DIRECTORY AbSets, BiRels, LichenDataOps, LichenDataStructure, LichenIntBasics, Process, Rope, SetBasics;

LichenChecking: CEDAR PROGRAM
IMPORTS AbSets, BiRels, LichenDataStructure, LichenIntBasics, Process, SetBasics
=

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.labelCellTypes.Difference[d.cellTypes].NonEmpty 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.ciXfm#nilBiRel 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.ciXfm#nilBiRel AND d.ciXfm.Scan[CheckCIXfm].found THEN ERROR;
Process.CheckForAbort[];
IF d.cellTypes.Scan[PerCellType].found THEN ERROR;
Process.CheckForAbort[];
RETURN};

CheckCellType: PUBLIC 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"];
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[];
IF pc IN PWClass THEN {
pwc: PWClass ~ pc;
bothd: Set ~ ct.isDeduced[pwc][FALSE].Intersection[ct.isDeduced[pwc][TRUE]];
IF bothd.NonEmpty THEN Error["Broken"];
{byd: Set ~ ct.isDeduced[pwc][FALSE].Union[b: ct.isDeduced[pwc][TRUE], disjoint: TRUE];
IF NOT byd.Equal[ct.CTParts[pc]] THEN Error["Broken"];
}};
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];
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];
physd: BOOL ~ a.offsets#NIL;
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 (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.
ZLichenChecking.Mesa
Last tweaked by Mike Spreitzer on July 25, 1988 11:59:18 am PDT
Κΰ–

"cedar" style˜
code™K™?—K˜KšΟk	œ_˜hK˜šΡbnxœœ
˜KšœI˜PKš
œ
˜
—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šœ3œ
œ˜PKšœ"œ
œ
˜/Kš
œ˜Kšœ"œ
œ
˜/Kš
œ˜šœœ˜!šŸœœœœ˜5Kšœ
œœ˜#Kšœœ
œ˜'Kš
œœ
œœ
œ˜Sšœœ˜Kšœ
œ!œ
œ˜BKš
œœ
œ œ
œ˜W—Kšœœ˜—Kšœ œ
œ
˜-Kš
œ˜Kšœ
˜—Kšœ"œ
œ
˜/Kš
œ˜Kšœ"œ
œ
˜/Kš
œ˜Kšœ&œ
œ
˜3Kš
œ˜Kšœœ œ
œ
˜BKš
œ˜Kšœ%œ
œ
˜2Kš
œ˜Kšœ˜—K˜šŸ
œœ
œ˜-K˜Kšœœœ
˜Kšœ	œœ
˜!Kšœ
œœ˜4Kšœ
œœ˜Bšœœ˜!šŸ
œœœœ˜:Kšœœ
˜Kšœ
œœ
œ
˜,Kšœœ˜—Kšœ$œœ˜EKšœœ+œ
œ
˜UKš
œ˜šœœ	œ˜Kš
œ˜Kšœœ!œ˜LKšœœ˜'Kšœœœ
œ˜WKšœ
œœ˜6K˜—Kšœ
˜—šœœ˜š
Ÿ
œœ Πcm
 œ œ˜OšŸ
œœœœ˜7Kšœ
œœ˜ Kšœ
œ
œ˜!Kšœ
œœ
œ
˜&Kšœœ˜—Kšœœ.œ˜aKšœœ
œ
˜+Kšœ˜—šŸœœœ
œ˜$Kšœœ˜Kš
œ˜Kš
œ)˜)Kšœ˜—šŸ	œœœœ˜3Kšœ
œœ˜šŸ
œœœœ˜7Kšœ
œœ˜ šœ
œ
œ
˜Kšœœ
œœ˜EKšœœœœ
œœ˜fKšœœ
˜—Kšœœ˜—Kšœ œ
œ
˜-Kšœœ˜—Kš
œ ˜ Kš
œ˜Kšœ%œ
œ
˜2Kš
œ˜Kš
œ.˜.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šœ
˜—…—!–-Π