Implementation details of Aignet's representation for execution. Since these details are hidden, most users can safely skip this section.
We now describe the actual implementation of the
The Aignet network consists mainly of an array of nodes representing a topologically sorted DAG.
Each node in the graph has an ID, which is a natural number that can be used to look up that node in the array. However, often our functions take arguments that may be a node or its negation; we encode this as a literal, as 2*ID+NEG, where NEG is 1 signifying negated or 0 signifying not negated.
One arbitrary well-formedness condition that we impose on all Aignet networks is that it must have a unique constant-false node with index 0. Therefore, the literal 0 is constant-false (the constant-false node, not negated), and the literal 1 is constant-true (the constant-false node, negated).
Information about each node is stored in the node array as two consecutive 32-bit numbers, and the node ID corresponds to its position in the array. That is, the two array indices of a node are 2*ID and 2*ID+1.
The two 32-bit values contained at these locations are broken down into two 30-bit data slots and four extra bits. Three of the four extra bits encode the type of the node, and the last extra bit encodes the phase of the node, which is its value when all inputs/registers are 0. The meaning of the 30-bit data slots depends on the type of node; in some cases it stores a literal.
The encoding is broken down, least-significant bits first, as follows:
|Data slot 0
|Data slot 1
The combinational types are encoded as follows:
The register flag only applies to combinational inputs/outputs; it should be 0 for constants/gates (but should also be ignored in those cases). Note that the polarity here can be very confusing:
The reason for this is described in aignet: the output of a register is an input to the combinational logic, and the input to a register is an output from the combinational logic.
So there are, in total, six types of objects, encoded as follows:
Only objects with combinational types 0, 1, and 2—constants, gates, and combinational inputs—may be fanins (descendants) of AND or combinational output objects; combinational outputs (type 3) may not.
The meanings of the two 30-bit data slots vary based on the type:
Having separate register input and output objects is somewhat awkward in terms of saying when a network is well-formed. In some sense, it's not well-formed unless every RO has a corresponding RI. But the RIs can't be added until their input cones are built, and we'd like to be able to say the network is well-formed in some sense while it is being built. So while an RO has no corresponding RI, we will say it is simply not updated: its value under sequential evalutation remains the same at each frame. A separate predicate can check that this isn't the case, but we won't generally require this for guards etc.
Furthermore, for convenience, we also allow RIs with fanin 1 set to 0. In this case they are not proper RIs because they do not connect to an RO, and they have no register number. They are also basically irrelevant to any sequential computation, because no RI gets updated with their previous value.
We require that each RI object occur later (have a larger ID) than its corresponding RO object. This allows a couple of conveniences:
Also, a strategy that might alleviate any inconvenience due to needing to add the RO before the RI: at the point of adding the RI, check whether the RO already exists and add it first if not.
An Aignet network is designed to have objects added one at a time without later modification. That is, new objects may be added, but existing objects are not changed. The object array itself (along with its size) contains enough information to fully replicate the network; in this sense, all other information recorded is auxiliary.
For efficient lookups, we do also keep arrays of inputs, outputs, and registers.
The input and output arrays simply hold the IDs of inputs/outputs in the order that they were added (as described above, each input/output object records its input/output numbers, i.e. the index in the input/output array that points back to it).
The register array is a bit more complicated, because there are typically two nodes (register input and register output) associated with each register. Each entry in the register array contains the ID of either a register input or output. If it is a register input, then the register is incomplete, i.e. its output hasn't been added yet. If it is a register output, then we have a complete register: the register array points to the register output node, which points to the register input node, which has the index in the register array.
For the full details, see the source code in