-- ChipDRCImpl.mesa

-- last modified by E. McCreight, January 30, 1984  6:16 PM
-- written by E. McCreight, April 14, 1982  10:25 AM

DIRECTORY
  ChipDRC,
  ChipFeature,
  ChipNetDefs,
  ChipWire,
  LeftFeaturePQ,
  FeaturePST,
  ppdefs,
  RightFeaturePQ,
  StreamDefs;

ChipDRCImpl: PROGRAM
  IMPORTS ChipDRC, ChipFeature, ChipNetDefs,
    ChipWire, LeftFeaturePQ, FeaturePST, RightFeaturePQ
  EXPORTS ChipDRC SHARES ChipDRC =
  BEGIN OPEN ppdefs, ChipNetDefs,
    FeaturePST, LeftFeaturePQ, RightFeaturePQ,
    ChipWire, ChipDRC;

  drcSwathWidth: PUBLIC Coord;

  doingDRC: PUBLIC BOOLEAN _ FALSE;

  polyGateOverlap, minTransistorDiffusionWidth,
    depletionOverlap: PUBLIC locNum;

  minSize, closestUnconnected:
    PUBLIC ARRAY ExtractLevel OF Coord;

  drcSwath: PUBLIC ChipWire.SlicePtr; -- drcSwathWidth wide
  drcSwathFeatures: PUBLIC RightFeaturePQHandle;
    -- the features in the slice but abandoned by ExtractNets

  SetupDRC: PUBLIC PROCEDURE[check: BOOLEAN] =
    BEGIN
    IF (doingDRC _ check) THEN
      BEGIN
      SetDRCParams[];
      holdViolations _ NOT HeSetsParamsAndSaysYes[
        "Should I tell you about errors as I find them?"];
      drcSwath _ ChipWire.NewSlice[];
      drcSwathFeatures _ NewRightFeaturePQ[uz];
      END;
    END; -- of SetupDRC


  FinishDRC: PUBLIC PROCEDURE[root: CellCallPtr] =
    BEGIN
    IF doingDRC THEN
      BEGIN
      PurgeSwath[LAST[Coord]];
      drcSwath _ ChipWire.DestroySlice[drcSwath];
      drcSwathFeatures _ DestroyRightFeaturePQ[drcSwathFeatures];
      END;
    CheckTerminalConnections[root];
    EnumerateViolations[];
    END; -- of FinishDRC


  LeftEdges: PUBLIC PROCEDURE[pq: LeftFeaturePQHandle] =
    BEGIN

    EnterSwath: PROCEDURE[f: FeaturePtr] =
      BEGIN
      rLev: ExtractLevel;
      IF InverseRequiredLevel[f.lev]=unknown THEN
        InsertFeaturePST[p: drcSwath[f.lev], item: f];
      IF (rLev _ RequiredLevel[f.lev])#unknown THEN
        NoteCover[lev: rLev, c: f.cover];
      END;

    CheckLeftEdge: PROCEDURE[f: FeaturePtr] =
      BEGIN
      lev, rLev, fLev: ExtractLevel;

      ForbiddenHere: PROCEDURE[item: FeaturePtr] =
        BEGIN
        p: Point;
        IF NOT HaveSharedArea[f.cover, item.cover] THEN RETURN;
        p _ RefCoordPt[SharedArea[f.cover, item.cover]];
        IF f.net=NIL OR item.net=NIL THEN
          NoteViolation[[place: p, info: coverageForbidden[lev: lev]]]
        ELSE -- it's a violation only if they're not the same
          IF (f.net _ CanonNet[f.net])#
            (item.net _ CanonNet[item.net]) THEN
            BEGIN
            id: NormalNetIdPtr = GetNormalNetId[@f.net];
            id.violations _ uz.NEW[ViolationList _ [
              next: id.violations,
              v: [place: p, info: coverageForbiddenIfNetsDiffer[lev: lev,
                n1: RefCanonNet[item.net], n2: RefCanonNet[f.net]]]]];
            END;
        END;

      IF (rLev _ InverseRequiredLevel[f.lev])#unknown THEN
        EnsureCoverage[lev: rLev, xNow: f.cover.x1,
          r: f.cover, NoCoverage: CoverageFailed];

      lev _ f.lev;
      IF (fLev _ ForbiddenLevel[f.lev])#unknown THEN
        SearchFeaturePST[p: drcSwath[fLev],
          int: [f.cover.y1, f.cover.y2],
          touch: ForbiddenHere]
      ELSE IF (lev _ InverseForbiddenLevel[f.lev])#unknown THEN
        SearchFeaturePST[p: drcSwath[lev],
          int: [f.cover.y1, f.cover.y2],
          touch: ForbiddenHere];

      IF closestUnconnected[f.lev]>0 THEN
        NeighborCheck[f: f, inLevel: f.lev, dist: closestUnconnected[f.lev]];

      SELECT f.lev FROM
        bur =>
          BEGIN
          NeighborCheck[f: f, inLevel: nGate, dist: (3*Lambda)/2];
          NeighborCheck[f: f, inLevel: pGate, dist: (3*Lambda)/2];
          END;
        nPlus => NeighborCheck[f: f, inLevel: pwelCont, dist: 3*Lambda];
        pPlus => NeighborCheck[f: f, inLevel: nwelCont, dist: 3*Lambda];
        pwelCont => NeighborCheck[f: f, inLevel: nPlus, dist: 3*Lambda];
        nwelCont => NeighborCheck[f: f, inLevel: pPlus, dist: 3*Lambda];
        ENDCASE => NULL;

      IF 0<minSize[f.lev] THEN
        LeftEdgeSizeCheck[f: f, minSize: minSize[f.lev]];
      END; -- of CheckLeftEdge

    x1: Coord _ LeftFeaturePQMin[pq].cover.x1;
    PurgeSwath[x1-drcSwathWidth];
    MapEqualLeftFeaturePQ[p: pq, proc: EnterSwath];
    MapEqualLeftFeaturePQ[p: pq, proc: CheckLeftEdge];
    END; -- of LeftEdges


  RightEdges: PUBLIC PROCEDURE[pq: RightFeaturePQHandle] =
    BEGIN

    CheckRightEdge: PROCEDURE[f: FeaturePtr] =
      BEGIN
      IF 0<minSize[f.lev] THEN
        RightEdgeSizeCheck[f: f, minSize: minSize[f.lev]];

      IF InverseRequiredLevel[f.lev]=unknown THEN
        InsertRightFeaturePQ[p: drcSwathFeatures, item: f]
      ELSE f _ ChipFeature.DestroyFeature[f];
      END; -- of CheckRightEdge

    x2: Coord _ RightFeaturePQMin[pq].cover.x2;
    PurgeSwath[x2-drcSwathWidth];
    MapEqualRightFeaturePQ[p: pq, proc: CheckRightEdge];
    END; -- of RightEdges


  PurgeSwath: PROCEDURE[x: Coord] =
    BEGIN
    WHILE RightFeaturePQSize[drcSwathFeatures]>0 AND
      RightFeaturePQMin[drcSwathFeatures].cover.x2<x DO
      oldF: FeaturePtr _ ExtractRightFeaturePQ[drcSwathFeatures];
      DeleteFeaturePST[p: drcSwath[oldF.lev], item: oldF];
      SELECT oldF.lev FROM
        nWellRequired, pWellRequired, nDepletionRequired,
          nBuriedContactRequired, nPlusRequired, pPlusRequired,
          nGateRequired, pGateRequired, polyRequired =>
          IF oldF.cover.x1<oldF.cover.x2 AND
            oldF.cover.y1<oldF.cover.y2 THEN
            NoteViolation[[place: RefCoordPt[oldF.cover],
              info: coverageNeeded[lev: InverseRequiredLevel[oldF.lev]]]];
        ENDCASE => NULL;
      oldF _ ChipFeature.DestroyFeature[oldF];
      ENDLOOP;
    END; -- of PurgeSwath

    -- Size checking ensures that connected
    -- features on the same layer are drawn
    -- so that a square of size minSize can be moved
    -- around every interior boundary of
    -- the connected region without getting stuck.

    -- Ramshaw and I spent a lunch brainstorming,
    -- and we decided that this
    -- is equivalent to every connected region's
    -- containing a square of size minSize on the interior of
    -- every corner.

    -- Corner are designated as {n, s}{e, w}{C, E}.
    -- (In Chipmonk's co-ordinate system, y increases
    -- southward and x increases eastward).
    -- For example, a nwC corner is a corner whose northwest
    -- quadrant is covered and all others are empty.  A seE corner
    -- is a corner whose southeast quadrant is empty and all others
    -- are covered.  There are eight of these designators, and
    -- a corner is completely determined by a point and a designator.


  LeftEdgeSizeCheck: PROCEDURE[f: FeaturePtr, minSize: Coord] =
    BEGIN

    LeftMinSizeViolation: PROCEDURE[lev: ExtractLevel,
      r: CoordRect] RETURNS[continue: BOOLEAN] =
      BEGIN
      MinSizeViolation[f: f, r: r];
      continue _ TRUE;
      END;

    r: CoordRect = f.cover;

    IF r.x1=r.x2 OR r.y1=r.y2 THEN RETURN;
      -- r is a point or a line.
      -- Such features correspond to required areas, whose absence
      -- is detected in other ways.

    -- r is known to be a non-empty area
    IF r.y2<r.y1+minSize
      AND NOT Covered[p: [r.x1, r.y1-1], lev: f.lev]
      THEN -- [r.x1, r.y1] is a seC corner
      EnsureCoverage[lev: f.lev, xNow: r.x1+1,
        r: [x1: r.x1,
          y1: r.y1,
          x2: r.x1+1,
          y2: r.y1+minSize],
          NoCoverage: LeftMinSizeViolation];
    END; -- of LeftEdgeSizeCheck

  RightEdgeSizeCheck: PROCEDURE[f: FeaturePtr, minSize: Coord] =
    BEGIN
    rightCover: Interval; -- [min..max)
    r: CoordRect = f.cover;

    RightMinSizeViolation: PROCEDURE[lev: ExtractLevel,
      r: CoordRect] RETURNS[continue: BOOLEAN] =
      BEGIN
      MinSizeViolation[f: f, r: r];
      continue _ TRUE;
      END;

    ExtendRightYCover: PROCEDURE[item: FeaturePtr] =
      BEGIN -- item's come in increasing order of item.cover.y1
      IF r.x2<item.cover.x2 AND
        rightCover.max<=r.y2 THEN
        BEGIN
        IF item.cover.y1<=rightCover.max THEN
          -- extend previous right cover
          rightCover.max _
            MAX[rightCover.max, item.cover.y2]
        ELSE
          BEGIN
          CheckRightCoverAndGap[item.cover.y1];
          rightCover _ [min: item.cover.y1, max: item.cover.y2];
          END;
        END;
      END; -- of ExtendRightYCover

    CheckRightCoverAndGap: PROCEDURE[nextCover: Coord] =
      BEGIN
      -- When this procedure is called,
      --  [rightCover.min..rightCover.max) is covered, and
      --  [rightCover.max..nextCover) is a gap.

      -- This procedure checks the following possibilities:
      --  1)  [x: r.x2, y: r.y1] is a swC corner
      --  3)  [x: r.x2, y: rightCover.max-1] is a seE corner
      --  4)  [x: r.x2, y: nextCover] is a neE corner
      --  6)  [x: r.x2, y: r.y2-1] is a nwC corner

      SELECT rightCover.max FROM
        <r.y1 => 
          -- [x: r.x2, y: r.y1] could be a swC corner
          IF (r.y2<r.y1+minSize OR
            r.x2<r.x1+minSize)
              -- f is not large enough by itself
            AND r.y1<nextCover -- no cover to the southeast
            AND NOT Covered[p: [x: r.x2-1, y: r.y1-1],
              lev: f.lev] -- no cover to the northwest
            THEN
            BEGIN
            EnsureCoverage[lev: f.lev, xNow: r.x2+1,
              r: [x1: r.x2-minSize,
                y1: r.y1,
                x2: r.x2,
                y2: r.y1+minSize],
                NoCoverage: RightMinSizeViolation];
            END;
      <r.y2 =>
        -- [x: r.x2, y: rightCover.max-1] is a seE corner
        EnsureCoverage[lev: f.lev, xNow: r.x2+1,
          r: [x1: r.x2-minSize,
            y1: rightCover.max-minSize,
            x2: r.x2,
            y2: rightCover.max],
            NoCoverage: RightMinSizeViolation];
      ENDCASE => NULL;

    SELECT nextCover FROM
      <=r.y1 => NULL;
      <r.y2 => 
        -- [x: r.x2, y: nextCover] is a neE corner
        EnsureCoverage[lev: f.lev, xNow: r.x2+1,
          r: [x1: r.x2-minSize,
            y1: nextCover,
            x2: r.x2,
            y2: nextCover+minSize],
            NoCoverage: RightMinSizeViolation];
      ENDCASE =>
        -- [x: r.x2, y: r.y2-1] could be a nwC corner
        IF (r.y2<r.y1+minSize OR
          r.x2<r.x1+minSize)
           -- f is not large enough by itself
         AND rightCover.max<r.y2 -- no cover to the northwest
         AND NOT Covered[p: [x: r.x2-1, y: r.y2],
               lev: f.lev] -- no cover to the southwest
         THEN
         EnsureCoverage[lev: f.lev, xNow: r.x2+1,
           r: [x1: r.x2-minSize,
             y1: r.y2-minSize,
             x2: r.x2,
             y2: r.y2],
             NoCoverage: RightMinSizeViolation];
      END; -- of CheckRightCoverAndGap

    IF r.x1=r.x2 OR r.y1=r.y2 THEN RETURN;
      -- r is a point or a line.
      -- Such features correspond to required areas, whose absence
      -- is detected in other ways.

    -- r is known to be a non-empty area
    rightCover _ [min: r.y1-1, max: r.y1-1];
    SearchFeaturePST[p: drcSwath[f.lev],
      int: [min: r.y1-1, max: r.y2+1],
      touch: ExtendRightYCover];
    IF rightCover.max<=r.y2 THEN
      CheckRightCoverAndGap[r.y2+1];
    END; -- of RightEdgeSizeCheck


  Covered: PROCEDURE[p: CoordPoint, lev: ExtractLevel]
    RETURNS[covered: BOOLEAN] =
    BEGIN

    CheckXCover: PROCEDURE[item: FeaturePtr] =
      {IF p.x IN [item.cover.x1..item.cover.x2) THEN
        covered _ TRUE};

    covered _ FALSE;
    SearchFeaturePST[p: drcSwath[lev],
      int: [min: p.y, max: p.y+1],
      touch: CheckXCover];
    END; -- of Covered


  MinSizeViolation: PROCEDURE[f: FeaturePtr, r: CoordRect] =
    BEGIN
    v: Violation = [place: RefCoordPt[r], info: tooNarrow[lev: f.lev]];
    IF f.net#NIL THEN
      BEGIN
      cn: CanonNetPtr _ f.net _ CanonNet[f.net];
      WITH did: cn.id SELECT FROM
        normal =>
          IF did.couldBeLogo THEN
            {did.violations _ uz.NEW[ViolationList _ [ next: did.violations, v: v ]]; RETURN};
        ENDCASE => NULL;
      END;
    NoteViolation[v];
    END; -- of MinSizeViolation

  NeighborCheck: PROCEDURE[f: FeaturePtr, inLevel: ExtractLevel, dist: Coord] =
    BEGIN

    TooCloseViolation: PROCEDURE[neighbor: FeaturePtr] =
      BEGIN
      cnNeighbor: CanonNetPtr _ neighbor.net _
        CanonNet[neighbor.net];
      v: Violation _ [
        place: RefCoordPt[[
          x1: MIN[f.cover.x1, neighbor.cover.x2],
          x2: f.cover.x1,
          y1: MAX[f.cover.y1-dist, neighbor.cover.y1],
          y2: MIN[f.cover.y2+dist, neighbor.cover.y2]]],
        info: tooClose[lev1: f.lev, lev2: neighbor.lev,
          n1: (f.net _ RefCanonNet[f.net]), n2: RefCanonNet[cnNeighbor]]];
      IF f.cover.x1<=cnNeighbor.id.final.r.x2 OR
        (GetNormalNetId[@f.net].couldBeLogo AND
        GetNormalNetId[@neighbor.net].couldBeLogo) THEN
        -- nets could still not be in error
        cnNeighbor.id.violations _ uz.NEW[ViolationList _
          [next: cnNeighbor.id.violations, v: v]]
      ELSE NoteViolation[v];
      END; -- of TooCloseViolation

    CheckNeighborDiffusion: PROCEDURE[item: FeaturePtr] =
      BEGIN
      cnitem: CanonNetPtr _ item.net _ CanonNet[item.net];

      ASSERT[item.cover.x1<=f.cover.x1];

      IF f#item AND f.cover.x1<item.cover.x2+dist AND
        cnitem#cnf AND item.lev=f.lev THEN
        -- Min separation is not violated if there is poly
        -- between the two diffused regions
        BEGIN

        polyPossible: BOOLEAN _ TRUE;

        PolyNotPossible: PROCEDURE[lev: ExtractLevel, r: CoordRect]
          RETURNS[continue: BOOLEAN] =
          {continue _ polyPossible _ FALSE};

        polyX: Interval = IF item.cover.x2<f.cover.x1 THEN
            -- x intervals don't overlap
            [min: item.cover.x2, max: f.cover.x1]
          ELSE
            [min: f.cover.x1-polyGateOverlap,
            max: MIN[f.cover.x2, item.cover.x2]+polyGateOverlap];
        polyY: Interval = IF item.cover.y2<f.cover.y1 OR f.cover.y2<item.cover.y1 THEN
            -- y intervals don't overlap
            [min: MIN[f.cover.y2, item.cover.y2],
            max: MAX[f.cover.y1, item.cover.y1]]
          ELSE
            [min: MAX[f.cover.x1, item.cover.x1]-polyGateOverlap,
            max: MIN[f.cover.x2, item.cover.x2]+polyGateOverlap];
        polyCover: CoordRect =
          [x1: polyX.min, y1: polyY.min, x2: polyX.max, y2: polyY.max];

        EnsureCoverage[lev: poly, xNow: f.cover.x1+1,
          r: [x1: polyCover.x1, x2: MIN[polyCover.x2, f.cover.x1+1],
            y1: polyCover.y1, y2: polyCover.y2],
          NoCoverage: PolyNotPossible];
          -- see if poly coverage appears likely ... may make polyPossible FALSE

        IF polyPossible THEN
          EnsureCoverage[lev: poly, xNow: f.cover.x1,
            r: polyCover, NoCoverage: CoverageFailed]
        ELSE TooCloseViolation[item];
        END;
      END; -- of CheckNeighborDiffusion

    CheckThisNeighbor: PROCEDURE[item: FeaturePtr] =
      BEGIN
      cnitem: CanonNetPtr _ item.net _ CanonNet[item.net];
      IF f#item AND f.cover.x1<item.cover.x2+dist AND
        cnitem#cnf THEN
          TooCloseViolation[item];
      END; -- of CheckThisNeighbor

    cnf: CanonNetPtr _ f.net _ CanonNet[f.net];
    SearchFeaturePST[p: drcSwath[inLevel],
      int: [min: f.cover.y1-dist, max: f.cover.y2+dist],
      touch:
        (SELECT f.lev FROM
          nPlus, pPlus => CheckNeighborDiffusion, -- transistors interfere
          ENDCASE => CheckThisNeighbor)
      ];
    END; -- of NeighborCheck

  maxNeedingCover: CARDINAL = 100;
  needCover, oldNeedCover: ARRAY[0..maxNeedingCover)
    OF CoordRect;
  numNeedingCover: [0..maxNeedingCover];


  EnsureCoverage: PROCEDURE[lev: ExtractLevel, xNow: Coord,
    r: CoordRect,
    NoCoverage: PROCEDURE[lev: ExtractLevel, r: CoordRect]
      RETURNS[continue: BOOLEAN]] =
    BEGIN
    -- Any x-values less than xNow will certainly already be present
    -- in the swath.  x-values greater than or equal to
    -- xNow might be present in
    -- the swath, but need not yet be present.
    NeedCoverFull: SIGNAL = CODE;


    ExtendCoverage: PROCEDURE[item: FeaturePtr] =
      BEGIN
      c: CoordRect _ item.cover;
      source: [0..maxNeedingCover);
      nextSink: [0..maxNeedingCover] _ 0;
      
      StillNeedCover: PROCEDURE[r: CoordRect] = INLINE
        BEGIN
        IF nextSink<maxNeedingCover THEN
          BEGIN
          needCover[nextSink] _ r;
          nextSink _ nextSink+1;
          END
        ELSE SIGNAL NeedCoverFull;
        END; -- of StillNeedCover

      IF item.cover.x2<=r.x1 OR r.x2<=item.cover.x1 THEN
        RETURN; -- no chance of any coverage
      FOR source IN [0..numNeedingCover) DO
        oldNeedCover[source] _ needCover[source];
        ENDLOOP;
      FOR source IN [0..numNeedingCover) DO
        nc: CoordRect _ needCover[source];
        IF nc.x1<c.x2 AND c.x1<nc.x2 AND
          nc.y1<c.y2 AND c.y1<nc.y2 THEN
            BEGIN -- they share area
            IF nc.x1<c.x1 THEN
              StillNeedCover[[x1: nc.x1, x2: c.x1,
               y1: nc.y1, y2: nc.y2]];
            IF c.x2<nc.x2 THEN
              StillNeedCover[[x1: c.x2, x2: nc.x2,
               y1: MAX[c.y1, nc.y1], y2: MIN[c.y2, nc.y2]]];
            IF nc.y1<c.y1 THEN
              StillNeedCover[[x1: nc.x1, x2: nc.x2,
                y1: nc.y1, y2: c.y1]];
            IF c.y2<nc.y2 THEN
              StillNeedCover[[x1: nc.x1, x2: nc.x2,
                y1: c.y2, y2: nc.y2]];
            END
        ELSE StillNeedCover[nc];
        ENDLOOP;
      numNeedingCover _ nextSink;
      END; -- of ExtendCoverage

    IF r.x2<=r.x1 OR r.y2<=r.y1 THEN RETURN;
    needCover[0] _ r;
    numNeedingCover _ 1;
    SearchFeaturePST[p: drcSwath[lev], int: [min: r.y1, max: r.y2],
      touch: ExtendCoverage !
      NeedCoverFull => 
        {NoteViolation[[place: RefCoordPt[r], info: cantCheck[]]];
        GOTO Overflow}];
    FOR i: [0..maxNeedingCover) IN [0..numNeedingCover) DO
      IF needCover[i].x1<xNow THEN
        BEGIN
        continue: BOOLEAN _
          NoCoverage[lev: lev, r: [
            x1: needCover[i].x1, x2: xNow,
            y1: needCover[i].y1, y2: needCover[i].y2]];
        IF NOT continue THEN RETURN;
        END
      ELSE IF xNow<needCover[i].x2 THEN
        BEGIN
        req: FeaturePtr _
          ChipFeature.NewFeature[cover: needCover[i],
            lev: RequiredLevel[lev]];
        InsertFeaturePST[p: drcSwath[req.lev], item: req];
        InsertRightFeaturePQ[p: drcSwathFeatures, item: req];
        END;
      ENDLOOP;
    EXITS Overflow => NULL;
    END; -- of EnsureCoverage


  maxfListSize: CARDINAL = 100;
  fList: ARRAY [0..maxfListSize) OF FeaturePtr;

  NoteCover: PROCEDURE[lev: ExtractLevel, c: CoordRect] =
    BEGIN
    fListSize: [0..maxfListSize] _ 0;

    ListTouchedRequirements: PROCEDURE[item: FeaturePtr] =
      BEGIN
      IF item.cover.x1<c.x2 AND c.x1<item.cover.x2 AND
        item.cover.y1<c.y2 AND c.y1<item.cover.y2 THEN
          BEGIN -- they share area
          fList[fListSize] _ item;
          fListSize _ fListSize+1;
          END;
      END; -- of ListTouchedRequirements

    WillStillNeedCover: PROCEDURE[r: CoordRect] =
      BEGIN
      req: FeaturePtr _
        ChipFeature.NewFeature[cover: r, lev: lev];
      InsertFeaturePST[p: drcSwath[req.lev], item: req];
      InsertRightFeaturePQ[p: drcSwathFeatures, item: req];
      END;

    SearchFeaturePST[p: drcSwath[lev], int: [min: c.y1, max: c.y2],
      touch: ListTouchedRequirements];

    FOR i: [0..maxfListSize) IN [0..fListSize) DO
      nc: CoordRect _ fList[i].cover;
      DeleteFeaturePST[p: drcSwath[lev], item: fList[i]];
      IF nc.x1<c.x1 THEN
        [] _ CoverageFailed[lev: InverseRequiredLevel[lev],
          r: [x1: nc.x1, x2: c.x1, y1: nc.y1, y2: nc.y2]];
      fList[i].cover _ [x1: MIN[c.x2, nc.x2], x2: nc.x2,
        y1: MAX[nc.y1, c.y1], y2: MIN[nc.y2, c.y2]];
        -- the section where y overlaps
      InsertFeaturePST[p: drcSwath[lev], item: fList[i]];
      IF nc.y1<c.y1 THEN
        WillStillNeedCover[[x1: c.x1, x2: nc.x2,
         y1: nc.y1, y2: c.y1]];
      IF c.y2<nc.y2 THEN
        BEGIN
        WillStillNeedCover[[x1: c.x1, x2: nc.x2,
          y1: c.y2, y2: nc.y2]];
        END;
      ENDLOOP;
    END; -- of NoteCover


  CoverageFailed: PROCEDURE[lev: ExtractLevel, r: CoordRect]
    RETURNS[continue: BOOLEAN] =
    BEGIN
    NoteViolation[[place: RefCoordPt[r], info: coverageNeeded[lev: lev]]];
    continue _ TRUE;
    END; -- of CoverageFailed


  RequiredLevel: PROCEDURE[lev: ExtractLevel]
    RETURNS[ExtractLevel] =
    {RETURN[(SELECT lev FROM
      nWell => nWellRequired,
      pWell => pWellRequired,
      nDepletion => nDepletionRequired,
      nBuriedContact => nBuriedContactRequired,
      nPlus => nPlusRequired,
      pPlus => pPlusRequired,
      nGate => nGateRequired,
      pGate => pGateRequired,
      poly => polyRequired,
      ENDCASE => unknown)]};


  InverseRequiredLevel: PROCEDURE[lev: ExtractLevel]
    RETURNS[ExtractLevel] =
    {RETURN[(SELECT lev FROM
      nWellRequired => nWell,
      pWellRequired => pWell,
      nDepletionRequired => nDepletion,
      nBuriedContactRequired => nBuriedContact,
      nPlusRequired => nPlus,
      pPlusRequired => pPlus,
      nGateRequired => nGate,
      pGateRequired => pGate,
      polyRequired => poly,
      ENDCASE => unknown)]};

  ForbiddenLevel: PROCEDURE[lev: ExtractLevel]
    RETURNS[ExtractLevel] =
    {RETURN[(SELECT lev FROM
      nWell => nWellForbidden,
      pWell => pWellForbidden,
      nDepletion => nDepletionForbidden,
      nBuriedContact => nBuriedContactForbidden,
      nPlus => nPlusForbidden,
      pPlus => pPlusForbidden,
      nGate => nGateForbidden,
      pGate => pGateForbidden,
      poly => polyForbidden,
      cut => cutForbidden,
      ENDCASE => unknown)]};

  InverseForbiddenLevel: PROCEDURE[lev: ExtractLevel]
    RETURNS[ExtractLevel] =
    {RETURN[(SELECT lev FROM
      nWellForbidden => nWell,
      pWellForbidden => pWell,
      nDepletionForbidden => nDepletion,
      nBuriedContactForbidden => nBuriedContact,
      nPlusForbidden => nPlus,
      pPlusForbidden => pPlus,
      nGateForbidden => nGate,
      pGateForbidden => pGate,
      polyForbidden => poly,
      cutForbidden => cut,
      ENDCASE => unknown)]};


  END. -- of ChipDRCImpl