<> <> Code: - = not relevent n = not thought about N = not understood u = allegedly somewhat understood U = allegedly understood b = implemented, but with suspected bug(s) I = implemented t = tested somewhat T = tested a lot WS = wire structure A = arrays M = meat (ports or wires are being created/deleted/merged) IntroCellType U WS:-, A:- ExtroCellType U WS:U, A:- Differentiate U WS:-, A:U Undifferentiate U WS:u, A:u Just verify structural equivalence, and smash types. Can deduce port equivalences bottom-up! LowerChildren t WS:u, A:U, M:N RaiseGrandchildren t WS:u, A:U, M:N MergeTypes n WS:u, A:u, M:N SplitType t WS:u, A:I, M:N GroupUnorganized I WS:u, A:u, M:N Implemented in terms of LowerChildren + trivia that look insensitive to wire structure but sensitive to array issues. ExpandUnorganized u WS:u, A:u, M:N ExpandVertex I WS:b, A:u, M:N ExpandChildren u WS:u, A:u, M:N Flatten I WS:u, A:u, M:N Implemented in terms of ExpandVertex + trivia that look insensitive to wire structure but sensitive to array issues. RenameSteps t WS:t, A:t PrefixifyDesign T WS:-, A:T InheritNames T WS:-, A:T AddDeducedStructureToDesign T WS:t, A:T ReOrderDesign T WS:T, A:T 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 tagged hierarchy TH2 results from removing the cell instance ci of a port>joined cell type from the tagged hierarchy TH1 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; and Tags2 differs from Tags1 by not mapping ci, and by additionally mapping each member x of newcis W newws to the tag which results from concatenating Tags1 ci, {2ci3}, and Tags1 x. The tagged hierarchy TH2 results from flattening>out the port>joined cell type ct from the tagged hierarchy TH1 iff TH2 is the result of successively removing every instance of ct from TH1, in any order. (Do I need to prove that order is irrelevent?) In general, the tagged hierarchy TH2 results from flattening>out any subset CI' of the cell instances of the tagged hierarchy TH1 iff TH2 is the result of successively removing every instance in CI' from TH1 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 tagged hierarchy TH2 results from raising the set gcs of fully exposed cell instances in the tagged hierarchy TH1 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; Tags2 differs from Tags1 by: A) not mapping the members of gcs, and by B) additionally mapping each member newci of newcis, where newci ~ 2kid, gc3, to the concatenation of Tags1 kid, {2kid3}, and Tags1 gc. 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. Note that because of the tags, this relation can only be "run" one way. The tagged hierarchy TH2 results from grudgingly exposing the cell instance ci in the tagged hierarchy TH1 iff TH2 results from exporting the private wires connected at ci in TH1. 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 tagged hierarchy TH2 results from sweetly exposing the cell instance ci in the tagged hierarchy TH1 iff TH2 results from fully exporting the PU>closure of the private wires connected at ci in TH1. This preserves more wire structure than grudging exposure. I think that flattening out a port>joined cell type with no falsely mixed wires is equivalent to sweetly exposing, and raising, its subcells in any order, and then deleting the cell type % NOT TRUE! a truly mixed wire in the original state, all of whose private atoms are connected to subcells, would be exported by the latter but not the former. The tagged hierarchy TH2 results from exporting the subset W' of the non>public wires of some cell type ct in the tagged hierarchy TH1 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; and Tags2 differs from Tags1 by additionally mapping each member w of newws to the concatenation of Tags1 ci, {2ci3}, and Tags1 w', where ci is an instance of ct and w' is connected through ci to w (according to H2). 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 tagged hierarchy TH2 results from fully exporting the subset W' of the non>public wires of some cell type ct in the tagged hierarchy TH1 iff: TH2 results from exporting the subset W' of the non>public wires of ct in the tagged hierarchy TH1; 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 tagged hierarchy TH2 results from sweeping up the lonely wire forest W' of the cell type ct in the tagged hierarchy TH1 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; and Tags2 differs from Tags1 by not mapping any member of P' or W'. The tagged hierarchy TH2 results from raising the set gcs of cell instances in the tagged hierarchy TH1 iff there exist tagged hierarchies TH1.3 and TH1.6 such that: TH1.3 results from sweetly exposing the cell instances gcs in TH1; TH1.6 results from raising the gcs in TH1.3; and TH2 results from sweeping up all the lonely wire trees of the childType in TH1.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 tagged hierarchy TH2 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 tagged hierarchy TH1 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 TH1 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 TH1 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; Tags2 differs from Tags1: A) by removing the wires of ctw from the domain; B) by adding mappings from newwsu to the Tags1 of their ~u>mappings; C) by adding mappings from newwsv to the Tags1 of their ~v>mappings. The tagged hierarchy TH2 results from splitting the cell type ctw into the cell types ctu (containing subcells CIu) and ctv (containing subcells CIv) in the tagged hierarchy TH1 iff there exists tagged hierarchy TH1.5 such that: TH1.5 is the result of fully exporting the non>public wires that relatively bridge CIu and CIv; and TH2 is the result of splitting the cell type ctw by CIu and CIv in TH1.5. O the non>public wires that relatively bridge CIu and CIv are exportable. The tagged hierarchy TH2 results from liberally splitting the cell type ctw by CIu and CIv in the tagged hierarchy TH1 iff there exists tagged hierarchy TH1.5 such that: TH1.5 is the result of splitting the cell type ctw by CIu and CIv into ctu and ctv in TH1; TH2 is the result of splitting off some of the instances of ctu and ctv from TH1.5. The tagged hierarchy TH2 results from splitting off some of the cell instances CI' from TH1 iff: TH2 = TH1; or there exists CI'' and TH1.5 such that: CI'' Y CI'; CI'' Y the subcells of some ctw in TH1; CI' - CI'' contains no ancestors or siblings of members of CI''; TH1.5 results from liberally splitting ctw by CI'' in TH1; and TH2 results from splitting off some of the cell instances CI' - CI'' in TH1.5. The tagged hierarchy TH2 results from liberally raising the non-empty set gcs of cell instances in the tagged hierarchy TH1 iff there exists tagged hierarchy TH1.5 such that: TH1.5 is the result of raising the non-empty set gcs of cell instances in TH1; TH2 is the result of splitting off some of the new cell instances in TH1.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 set of sequences of cell instances is consistent iff in every pair of sequences that have some cell instances in common, those cell instances occur in the same relative order. A Tag is a consistent set of sequences of cell instances. The concatenation of one tag with another is the set of all concatenations of a sequence from the first tag and a sequence from the second tag. The union of two tags is just their set union. A tagged hierarchy TH is a tuple 2H, Tags3, where H is a hierarchy, and Tags is a function that maps each wire and cell instance in H to a Tag. The idea is that the tags relate H back to another hierarchy, from which it was produced by the structural manipulations discussed here. A hierarchy without wire structure is one in which all ports and wires are atomic. The tagged hierarchy TH2 is the result of removing wire structure from the tagged hierarchy TH1 iff TH2 is the result of removing every composite port and wire from TH1. The tagged hierarchy TH2 is the result of removing the composite ports P' and wires W' from the tagged hierarchy TH1 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; Tags2 differs from Tags1 by not mapping members of W'. The tagged hierarchy TH2 results from merging the wire sets W'' in the tagged hierarchy TH1 iff: W'' is a set of sets; each member W' of W'' is a set of wires; no two members of W'' have a non>empty intersection; Wu = the union of the sets in W''; Wu Y W1; there is a set of wires mws (which may or may not have some members in common with Wu) that can be put in a one>to>one correspondence ~ with the members of W''; CT2 = CT1; CI2 = CI1; W2 = W1 - Wu W mws; P2 = P1; Conn2 differs from Conn1 in that wherever Conn1 connects some port p at some site c to a wire w in some W', Conn2 connects to ~W'; Sub2 = Sub1 - Wu ´ (N ´ W1) W Sub12, where Sub12: maps a member mw of mws iff mw ~ a set W' of composite1 wires; and mw ~ a set W' of composite1 wires O µ w J W': width2 mw = width1 w; and µ 0 e i < width2 mw: Sub12(mw)(i) ~ some Wc', where Sub1(w)(i) J Wc'; Parts2 ct = Parts1 ct - Wu W a subset of mws; Type2 = Type1; there is a Tags12 that differs from Tags1 by not mapping members of Wu; and Tags2 differs from Tags12 by additionally mapping each member mw of mws to the union of the tags1 of the members of ~mw. This implies: letting wa y wb mean that wa and wb are both members of some W'; wa y wb O wa and wb are both parts of the same cell type; wa y wb O either (according to H1): wa and wb are both atomic, or wa and wb are both composite, have the same width n, and µ 0 e i < n, Sub1(wa)(i) y Sub1(wb)(i); wa y wb ¶ wa b wb ¶ both are children O they have different parents, and both parents are in some same W'. A set of ports P' is easily mergable iff at every cell type and instance, all members of P' that are connected are connected to the same wire. The tagged hierarchy TH2 results from easily merging the port sets P'' in the tagged hierarchy TH1 iff: P'' is a set of sets; each member P' of P'' is an easily mergable set of ports; no two members of P'' have a non>empty intersection; Pu = the union of the sets in P''; Pu Y P1; there is a set of ports mps (which may or may not have some members in common with Pu) that can be put in a one>to>one correspondence ~ with the members of P''; CT2 = CT1; CI2 = CI1; W2 = W1; P2 = P1 - Pu W mps; Conn2 differs from Conn1 in that wherever Conn1 connects some port p in some P' at some site c to a wire w, Conn2 connects ~P'; Sub2 = Sub1 - Pu ´ (N ´ P1) W Sub12, where Sub12: maps a member mp of mps iff mp ~ a set P' of composite1 ports; and mp ~ a set P' of composite1 ports O µ p J P': width2 mp = width1 p; and µ 0 e i < width2 mp: Sub12(mp)(i) ~ some Pc', where Sub1(p)(i) J Pc'; Parts2 ct = Parts1 ct - Pu W a subset of mps; Type2 = Type1; Tags2 = Tags1. This implies: letting pa y pb mean that pa and pb are both members of some P'; pa y pb O pa and pb are both parts of the same cell type; pa y pb O either (according to H1): pa and pb are both atomic, or pa and pb are both composite, have the same width n, and µ 0 e i < n, Sub1(pa)(i) y Sub1(pb)(i); pa y pb ¶ pa b pb ¶ both are children O they have different parents, and both parents are in some same P'. A set is non>trivial iff it has more than one member. The required wire merges of a set P'' of sets of ports in a hierarchy H is a set W'' of non>trivial sets of wires, such that at every cell type and instance, for every member P' of P'', either: all members of P' that are connected are connected are connected to the same wire, or the set of wires that are connected to members of P' is a member of W''.