[Pixel]<DATools7.0>Lichen>LichenDoc.Tioga!12

LichenDoc.Tioga

Last tweaked by Mike Spreitzer on February 23, 1988 5:44:50 pm PST

Issues in the formalization:

Should there be atomic cell types?

Should the tags be part of the hierarchy?

Should it allow empty composite ports & wires?

Should composite connectivity derive from atomic connectivity?

Should it allow split ports?

A hierarchy is a tuple H = 2CT, CI, W, P, Conn, Sub, Parts, Type3, where:

CT is a set of cell types;

CI is a set of cell instances;

W is a set of wires;

P is a set of ports;

Conn: P ´ (CT W CI) Ž W is a function that maps a port and a cell to a wire;

Sub: (PWW) Ž (N R (PWW)) maps a parent port or wire to the sequence of its children;

Parts: CT Ž (CI W P W W)* maps a cell type to the set of its ports, wires, and subcells;

Type: CI Ž CT maps a cell instance to the cell type of which it is an instance;

and with the following definitions:

the sites (for connection) of a cell type are itself and its instantiations;

an atomic port or wire is one that is not in the domain of Sub;

an empty port or wire is one that is mapped by Sub to the empty set;

a composite port or wire is in the domain of Sub;

empty, atomic, and composite are similarly defined for cell types and Parts;

the width of a composite port or wire is the number of its children;

a port p and wire w are connectable at a site c iff either:

both are atomic, or

both are composite, have the same width n, and ľ 0 e i < n: Sub(p)(i) and Sub(w)(i) are connected at c;

a wire is public iff it is connected at a cell type;

a cell type has split ports iff it has a wire connected to more that one port at the cell type;

the following constraints hold:

a port is connected only at a site of its cell type;

an atomic port is connected at every site of its cell type;

a wire is conected only at its cell type, or a subcell thereof;

a wire and port are connected at some site only if they are connectable there;

a wire or port has at most one parent & index combination;

the children of a port are ports, and the children of a wire are wires;

the children of a port or wire are parts of the same cell type as their parent;

the children of a port or wire are indexed by [0, n), for some n;

every member of CI W W W P is a part of exactly one cell type;

every cell instance has a type.

A top port or wire is one that has no parent (according to Sub); The topmost ports and wires of some set S are those that are not children of other members;

We say x is an ancestor of y when x=y or x is a parent of z and z is an ancestor of y. Here we take parenthood as given among ports and wires by Sub, and among cell types and instances as given by Parts and Type (an instance is a parent of its type; a subcell is a child of its containing type).

A wire is private iff it has no public descendants. A wire is mixed iff it is neither public nor private. A wire is truly mixed iff it has both public and private descendants. A wire is falsely mixed iff it is mixed, but all its children are public, and there's a port of the wire's containing cell type that is connectable to the wire. A wire is blockedly mixed iff it is mixed, but all its children are public, and there's no port of the wire's containing cell type that is connectable to the wire.

A wire w is exported through a port p if w is connected to p at some cell type. A wire w is connected through a cell instance ci to another wire w' iff w is exported through a port p and w' is connected to p at ci.

A cell type ct is port>joined iff it has no two ports that both export the same wire. A hierarchy is port>joined iff every cell in it is port>joined.

The hierarchy H2 results from deleting the cell type ct from the hierarchy H1 iff:

either ct is port>joined and has no subcells, or ct has no instances, in H1;

ct J CT1;

CT2 = CT1 - {ct};

CI2 = CI1 - instances1 of ct - subcells1 of ct;

W2 = W1 - wires of1 ct;

P2 = P1 - ports of1 ct;

Conn2 differs from Conn1 by excluding connections at ct, at instances of ct, and at subcells of ct;

Sub2 differs from Sub1 by not mapping parts of ct;

Parts2 differs from Parts1, if at all, by not mapping ct;

Type2 differs from Type1, if at all, by not mapping instances or subcells of ct.

The hierarchy H2 results from retyping the instance ci from ct to ct' in hierarchy H1 iff:

CT2 = CT1;

CI2 = CI1;

W2 = W1;

P2 = P1;

Conn2 = Conn1;

Sub2 = Sub1;

Parts2 = Parts1;

Type2 differs from Type1 only at ci;

Type1 ci = ct;

Type2 ci = ct';

ct and ct' are structurally equivalent in H1.

Two cell types cta and ctb are structurally equivalent iff:

there is a one-to-one relation ~ between the parts of cta and ctb, and between {cta} and {ctb};

~ relates wires to wires, ports to ports, cell types to cell types, and cell instances to cell instances;

ct J {cta, ctb} O [ Conn(p´ct)=w N Conn(~p´~ct)=~w ];

ci J subcells of cta W subcells of ctb O [ Conn(p´ci)=w N Conn(p´~ci)=~w ];

~ is an isomorphism for the Sub relation among the parts of cta and the Sub relation among the parts of ctb;

ci J subcells of cta W subcells of ctb O Type ci = Type ~ci.

The hierarchy H2 results from removing the cell instance ci of a port>joined cell type from the hierarchy H1 iff:

ct = Type1 ci;

ci J Parts1 cct

newcis = CI2 - CI1;

newws = W2 - W1;

CT2 = CT1;

CI2 = CI1 - {ci} W newcis;

W2 = W1 W newws;

P2 = P1;

a one>to>one relation ~ between newcis and the subcells of ct, and between newws and the private wires of ct, can be invented;

Conn2 differs from Conn1 by not having any connections at ci, and by additionally connecting some w to some p at some ci iff either (a) Conn1 connects p at ~ci to ~w, or (b) Conn1 connects w at ci to some p' and p' at ct to some w' and w' to p at ~ci;

Sub2 differs from Sub1 by additionally containing the ~>image of the Sub1 relation among the private wires of ct;

Parts2 differs from Parts1 only at cct, and there by removing ci and adding newws and newcis;

Type2 differs from Type1 by not mapping ci, and by additionally mapping each member of newcis to the type of its ~>mapping.

The hierarchy H2 results from flattening>out the port>joined cell type ct from the hierarchy H1 iff H2 is the result of successively removing every instance of ct from H1, in any order. (Do I need to prove that order is irrelevent?) In general, the hierarchy H2 results from flattening>out any subset CI' of the cell instances of the hierarchy H1 iff H2 is the result of successively removing every instance in CI' from H1 in a bottom>up order; all bottom>up orders give the same result (it has to be bottom>up because a higher flattening "replaces" some cell instances with others, and so may "mask" membership in CI').

A cell instance ci is fully exposed in a hierarchy H iff every atomic port of ci's type is connected at ci to a public wire.

The hierarchy H2 results from raising the set gcs of fully exposed cell instances in the hierarchy H1 iff:

the members of gcs are all parts of one cell type, which we'll call childType;

newcis = CI2 - CI1;

kids = the instances of childType;

CT2 = CT1;

CI2 = CI1 - gcs W newcis;

W2 = W1;

P2 = P1;

a one>to>one relation ~ between newcis and kids ´ gcs can be invented;

Conn2 differs from Conn1 by not having any connections at any member of gcs, and by adding, for each kid, gc, p, and w, where kid J kids, gc J gcs, p is connected1 at gc to w, and w is connected1 through kid to some wire, a connection at ~2kid,gc3 between p and some wire w' to which w is connected1 through kid.

Sub2 = Sub1;

Parts2 differs from Parts1 by omitting gcs from the parts of childType, and by distributing the members of newcis among the containing cell types of kids;

Type2 differs from Type1 by not mapping the members of gcs, and by additionally mapping each member newci of newcis to some gcType, where newci ~ 2some kid, an instance of gcType3.

There is a detail that is not nailed down here: which outside wire is used when an inside wire is connected to more than one port. There was a choice made here: how much composite wire structure to preserve, and the answer is: as much as possible.

The hierarchy H2 results from grudgingly exposing the cell instance ci in the hierarchy H1 iff H2 results from exporting the private wires connected at ci in H1.

The PU>closure of a set of non>public wires is another set of wires, wherein each member either:

is a member of the given set, or

is composite, is not public, has a child in the PU>closure, and has only children that are public or in the PU>closure.

The hierarchy H2 results from sweetly exposing the cell instance ci in the hierarchy H1 iff H2 results from fully exporting the PU>closure of the private wires connected at ci in H1.

The hierarchy H2 results from exporting the subset W' of the non>public wires of some cell type ct in the hierarchy H1 iff:

CT2 = CT1;

CI2 = CI1;

W2 = W1 W newws;

P2 = P1 W P';

newws V W1 = a;

each member of newws is connected in Conn2;

no member of P' is connected at ct in Conn1;

Conn2 differs from Conn1:

A) by some additional connections at ct, which form a one>to>one relation beween W' and P' (choice: introduce no split ports); and

B) by some additional connections, each of the form of connecting some port p in P' at some instance ci of ct to some wire w in newws (unspecified: how much composite port structure is preserved);

Sub2 differs by Sub1 by:

A) additionally mapping pp, only if (other direction is forced where appropriate by differences in Conn and well>formedness of H2) pp is in P2 - P1; and

B) additionally mapping wp, only if wp is in newws;

Parts2 differs from Parts1:

A) at ct, where it adds P2 - P1; and

B) by distributing the members of newws among the containing cell types of the instances of ct;

Type2 = Type1.

O every child of every composite member of W' is either public or in W'.

O every member of W' is exportable.

A wire is exportable iff every child of it is either public or exportable, and either:

there is a port to which the wire is connectable at the cell type; or

every connectable (at the cell type) child of the wire is connectable (at the cell type) to a top port.

The hierarchy H2 results from fully exporting the subset W' of the non>public wires of some cell type ct in the hierarchy H1 iff:

H2 results from exporting the subset W' of the non>public wires of ct in the hierarchy H1; and

every member of W' is connected through every instance of ct.

A wire tree is the set of descendants of some top wire. A wire forest is the union of some wire trees. Note that each wire is a member of exactly one tree. Similar dfinitions and observations hold for ports.

A wire is lonely iff no descendant is connected at a cell instance. A set of wires is lonely iff every member is.

The hierarchy H2 results from sweeping up the lonely wire forest W' of the cell type ct in the hierarchy H1 iff:

CT2 = CT1;

CI2 = CI1;

W2 = W1 - W';

P2 = P1 - P';

P' is a forest of ports of ct;

every wire connected to a member of P' at ct is a member of W';

Conn2 differs from Conn1 by omitting all connections of ports in P';

Sub2 differs from Sub1 by not mapping any member of P' or W';

Parts2 differs from Parts1 at ct by omitting P' and W';

Type2 = Type1.

The hierarchy H2 results from raising the set gcs of cell instances in the hierarchy H1 iff there exist tagged hierarchies H1.3 and H1.6 such that:

H1.3 results from sweetly exposing the cell instances gcs in H1;

H1.6 results from raising the gcs in H1.3; and

H2 results from sweeping up all the lonely wire trees of the childType in H1.6.

A wire bridges two sets of cell instances iff it has at least one connection in each set. A wire relatively bridges two sets of cell instances iff its tree contains a wire that bridges the two sets of cell instances.

The hierarchy H2 results from splitting the cell type ctw into the cell types ctu (containing subcells CIu) and ctv (containing subcells CIv), when all the wires of ctw that relatively bridge CIu and CIv are public, in the hierarchy H1 iff:

CIu W CIv = the subcells1 of ctw;

CT2 = CT1 - {ctw} W {ctu, ctv};

CI2 = CI1 - instances of ctw W instsu W instsv;

W2 = W1 - wires of ctw W newwsu W newwsv;

P2 = P1 - ports of ctw W newpsu W newpsv;

there is a one>to>one relation ~u:

beween instsu and the instances of ctw,

between newwsu and some of the wires of ctw, and

between newpsu and some of the ports of ctw;

there is a one>to>one relation ~v:

beween instsv and the instances of ctw,

between newwsv and some of the wires of ctw, and

between newpsv and some of the ports of ctw;

newwsu is closed upward and downward, as are newwsv, newpsu, and newpsv (choice: whether and how to split composite ports & wires);

Conn2 differs from Conn1:

A) by removing every connection at ctw, and then adding the ~u and ~v images of those connections at ctu and ctv;

B) for every connection in H1 between some port p and some wire w at some subcell ci of ctw by:

1) omitting that connection; and by then

2) adding a connection between p and some wire w' at ci, where w' ~u w if ci is in CIu, and w' ~v w if ci is in CIv;

C) for every connection in H1 between some port p and some wire w at some instance ci of ctw:

1) by omitting that connection;

2) by adding a connection between some pu and w at ~u ci iff pu ~u p;

3) by adding a connection between some pv and w at ~v ci iff pv ~v p;

Sub2 differs from Sub1 by not mapping any ports or wires of ctw, and then adding the ~u and ~v images of the Sub1 relation;

Parts2 differs from Parts1:

by not mapping ctw;

by mapping ctu to CIu W newpsu W newwsu;

by mapping ctv to CIv W newpsv W newwsv;

at each cell type ct that contains1 instances of ctw, by removing those instances, and then adding their ~u and ~v images;

Type2 differs from Type1 by removing the instances of ctw from the domain, then adding mappings from instsu to ctu and instsv to ctv.

Note that this does not nail down how much of the ports and wires are kept in each of the resulting cell types.

The hierarchy H2 results from splitting the cell type ctw into the cell types ctu (containing subcells CIu) and ctv (containing subcells CIv) in the hierarchy H1 iff there exists hierarchy H1.5 such that:

H1.5 is the result of fully exporting the non>public wires that relatively bridge CIu and CIv; and

H2 is the result of splitting the cell type ctw by CIu and CIv in H1.5.

O the non>public wires that relatively bridge CIu and CIv are exportable.

The hierarchy H2 results from liberally splitting the cell type ctw by CIu and CIv in the hierarchy H1 iff there exists hierarchy H1.5 such that:

H1.5 is the result of splitting the cell type ctw by CIu and CIv into ctu and ctv in H1;

H2 is the result of splitting off some of the instances of ctu and ctv from H1.5.

The hierarchy H2 results from splitting off some of the cell instances CI' from H1 iff:

H2 = H1; or

there exists CI'' and H1.5 such that:

CI'' Y CI';

CI'' Y the subcells of some ctw in H1;

CI' - CI'' contains no ancestors or siblings of members of CI'';

H1.5 results from liberally splitting ctw by CI'' in H1; and

H2 results from splitting off some of the cell instances CI' - CI'' in H1.5.

The hierarchy H2 results from liberally raising the non-empty set gcs of cell instances in the hierarchy H1 iff there exists hierarchy H1.5 such that:

H1.5 is the result of raising the non-empty set gcs of cell instances in H1;

H2 is the result of splitting off some of the new cell instances in H1.5.

A permutation map is a function from ports and wires to permutations.

The hierarchy H2 results from applying the permutation map PM to the hierarchy H1 iff:

dom PM Y the composite wires and ports of H1;

CT2 = CT1;

CI2 = CI1;

W2 = W1;

P2 = P1;

Conn2 = Conn1;

Sub2 differs from Sub1 at the domain of PM; at every such point x, Sub2 x = (PM x) g (Sub1 x);

Parts2 = Parts1;

Type2 = Type1.

A hierarchy without wire structure is one in which all ports and wires are atomic.

The hierarchy H2 is the result of removing wire structure from the hierarchy H1 iff H2 is the result of removing every composite port and wire from H1.

The hierarchy H2 is the result of removing the composite ports P' and wires W' from the hierarchy H1 iff:

P' Y P1;

W' Y W1;

P' and W' are closed upward (if a child is in, its parent is in);

CT2 = CT1;

CI2 = CI1;

W2 = W1 - W';

P2 = P1 - P';

Conn2 differs from Conn1 by omitting every connection for every port in P' and wire in W';

Sub2 differs from Sub1 by not mapping the ports in P' and wires in W';

Parts2 differs from Parts1 by omitting all the members of P' and W'; and

Type2 = Type1.

A set is non>trivial iff it has more than one member.