• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
          • Aignet-impl
            • Node
            • Network
            • Combinational-type
            • Stypep
            • Typecode
          • Aignet-copy-init
          • Aignet-simplify-marked-with-tracking
          • Aignet-cnf
          • Aignet-simplify-with-tracking
          • Aignet-complete-copy
          • Aignet-eval
          • Semantics
          • Aignet-transforms
          • Aignet-simplify-marked
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Representation

    Aignet-impl

    Implementation details of Aignet's representation for execution. Since these details are hidden, most users can safely skip this section.

    For background see aignet and representation.

    We now describe the actual implementation of the aignet stobj for execution. Our use of abstract-stobjs means that these details are completely hidden from reasoning about aignet and have nothing at all to do with the logical view of an aignet as a list of logical nodes. You should not need to know these details when writing new Aignet algorithms or when understanding existing Aignet code!

    Node Array

    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.

    Node Encoding

    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:

    Size Contents
    2 Combinational type
    30 Data slot 0
    1 Register flag
    1 Phase
    30 Data slot 1

    The combinational types are encoded as follows:

    Encoding Meaning
    0 Constant false
    1 And gate
    2 Input
    3 Output

    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:

    • An input with the register flag set is a register output,
    • An output with the register flag set is a register input.

    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:

    Name Combinational Type Register Flag
    Constant 0 -
    And gate 1 -
    Primary Input 2 0
    Register Output 2 1
    Primary Output 3 0
    Register Input 3 1

    Restrictions and Interpretation

    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:

    • Constants. Both data 0 slots are meaningless; they should be set to 0 and ignored.
    • AND gates. Data 0 and 1 are literals encoding the fanins to the gate. To ensure an obvious topological ordering, the ID part of each literal must be less than the gate ID.
    • Combinational inputs. Data 0 is ignored and should be 0. Fanin 1 gives the PI or register number, sequentially assigned and unique among PI/registers.
    • Primary outputs. Data 0 is the fanin (literal) of the output, whose ID must (for topological ordering) be less than the output node ID. Data 1 is the output number.
    • Register inputs. Data 0 is the fanin (literal) of the register, whose ID must (for topological ordering) be less than this node's ID. Fanin 1 is the ID of the corresponding register output, which must also be less than this node's ID. (The register number of the RI is the register number of the corresponding RO.)

    Register Considerations

    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:

    • There is a function for adding an RO and another function for adding an RI which connects it to an existing RO. If we allowed RIs to occur first, then we'd need an additional pair of functions, for adding an unconnected RI and for adding an RO connected to an RI. Maybe we could avoid this by separately allowing RO/RIs to be connected, but this seems knotty in terms of well-formedness.
    • When doing a sequential simulation or similar operation that involves repeated sweeps across the AIG nodes, an RO node will be reached before the corresponding RI's previous value is overwritten. So we don't need an addtional step of copying RI to RO values between frames.

    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.

    Other Arrays

    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.

    Source Code

    For the full details, see the source code in aignet-exec.lisp or aignet-exec-thms.lisp.