
    <<LichenChecking.Mesa>>
        <<Last tweaked by Mike Spreitzer on July 25, 1988 11:59:18 am PDT>>

    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 
                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.
                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.
            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.