Common Types
LORA: TYPE = LIST OF REF ANY;
ROPE: TYPE = Rope.ROPE;
RopeList: TYPE = LIST OF ROPE;
SymbolTable: TYPE = HashTable.Table;
Assertions: TYPE = Asserting.Assertions;
Random Connectivity
A random pile of boxes and wires is represented with a bipartate graph.
Vertex: TYPE = REF VertexPrivate;
VertexPrivate:
TYPE =
RECORD [
firstEdge, lastEdge: Edge ← NIL,
extraConnections: SymbolTable ← NIL,
names: RopeList ← NIL,
container: CellType,
other: Assertions ← NIL,
variant:
SELECT class: VertexClass
FROM
wire => [
parent: Wire ← NIL,
myIndex: NAT ← 0,
elts: SEQUENCE length: NAT OF Wire
],
cell => [
type: CellType ← NIL,
nextInstance, prevInstance: Vertex ← NIL
],
ENDCASE
];
VertexClass: TYPE = {wire, cell};
Wire: TYPE = REF WirePrivate;
WirePrivate: TYPE = VertexPrivate[wire];
CellInstance: TYPE = REF CellInstancePrivate;
CellInstancePrivate: TYPE = VertexPrivate[cell];
Edge: TYPE = REF EdgePrivate;
EdgePrivate:
TYPE =
RECORD [
sides: ARRAY VertexClass OF RECORD [v: Vertex, next, prev: Edge],
other: Assertions ← NIL,
portIndex: CARDINAL];
Ports
A port is a connection point on a CellType. Each port is connected to extactly one wire. A wire may be connected to any number of ports.
PortS: TYPE = REF PortSeq;
PortSeq: TYPE = RECORD [ports: SEQUENCE length: PortIndex OF Port];
PortIndex: TYPE = NAT;
NullPortIndex: PortIndex = LAST[PortIndex];
Port:
TYPE =
RECORD [
names: RopeList ← NIL,
netNames: RopeList ←
NIL,
The names of the wire this port is connected to.
other: Assertions ← NIL];
Array Connectivity
There is a special representation for array connectivity. There are constraints beyond what can be expressed with Cedar data types:
AA1: Each connection between adjacent elements involves exactly one port of each element.
AA2: Each port of an array connects to no more than one port of each element.
AA3: For any port of an array, all of the element ports it connects to are connected by array elements.
Array: TYPE = REF ArrayPrivate;
ArrayPrivate:
TYPE =
RECORD [
eltType: CellType,
shape: ARRAY Dim OF Range,
joints: ARRAY Dim--perp to joint-- OF ARRAY Phase--perp to dim-- OF ARRAY Phase--along dim-- OF Joint ← ALL[ALL[ALL[NIL]]],
portConnections: ArrayPortConnections,
redundant with porting.
porting:
SEQUENCE eltPorts: PortIndex
OF Porting
porting[p] gives port connections for e[f, b].p, for all f, b on edge of array.
];
Dim--ension--: TYPE = {Foo, Bar};
OtherDim: ARRAY Dim OF Dim = [Foo: Bar, Bar: Foo];
Range: TYPE = RECORD [min, maxPlusOne: INT];
Phase: TYPE = INTEGER [0 .. MaxPeriod);
MaxPeriod: INTEGER = 2;
Joint: TYPE = REF JointSeq;
JointSeq:
TYPE =
RECORD [joints:
SEQUENCE eltPorts: PortIndex
OF
RECORD [low, high: PortIndex]];
e[i].pl é e[i+1].ph { j[pl].high = ph ' j[ph].low = pl
e[i].pl not connected to any e[i+1].ph { j[pl].high = NullPortIndex
Porting: TYPE = REF ANY --actually UNION [{notPorted, unknownPorting}, DetailedPorting]--;
notPorted: Porting;
unknownPorting: Porting;
DetailedPorting: TYPE = REF DetailedPortingRep;
DetailedPortingRep:
TYPE =
RECORD [
corners:
ARRAY End
--Foo--
OF
ARRAY End
--Bar--
OF PortIndex,
e[Foo.LAST, Bar.LAST].p é a.q { porting[p].corners[high][high] = q
NullPortIndex means elt port not connected to any array port.
sideIndices:
ARRAY End
OF
ARRAY Dim
OF SideIndex,
sideIndices[low][Foo] covers [f, b] f = FIRST[Foo] ' b (FIRST[BAR] .. LAST[BAR])
slots: SEQUENCE length: NAT OF PortIndex];
End: TYPE = {low, high};
OtherEnd: ARRAY End OF End = [low: high, high: low];
SideIndex: TYPE = RECORD [same: BOOL, firstSlot: NAT];
ArrayPortConnections: TYPE = REF ArrayPortConnectionSeq;
ArrayPortConnectionSeq: TYPE = RECORD [SEQUENCE arrayPorts: PortIndex OF ARRAY End OF ARRAY Dim OF SideConnection];
SideConnection: TYPE = RECORD [range: Range, sockets: ArraySocketList];
ArraySocketList: TYPE = LIST OF ArraySocket;
ArraySocket: TYPE = RECORD [ai: ArrayIndex, pi: PortIndex];
ArrayIndex: TYPE = ARRAY Dim OF INT;