---- An Abstract Stobj Representation of And-Inverter Graphs ----

Outline:
Very basic intros:
  - Stobj?
  - Abstract stobj?
  - And/inverter graph?

AIGNET abstract stobj
  - Concrete representation
  - Example circuit's concrete representation
  - Abstract representation
  - Accessor/updater definitions
  - Advantages of abstract representation

-----

What's a stobj?
  - A destructively modifiable data structure that can be used in the ACL2 logic.
  - Can have scalar, array slots
  - Represented logically as a straightforward list-based model
         e.g., a 5-slot structure turns into a 5-element list
               an array slot of length N turns into a list of length N
     Accessors/updaters: nth, update-nth

What's an abstract stobj?
  - Have a regular (concrete) stobj as your implementation, but reason
about it as if it were some other kind of structure.
  - Nth/update-nth is a fiction anyway; abstract stobj lets you choose
an equally valid logical fiction to use (after some proofs).

What's an and/inverter graph?
  - Directed acyclic graph.  Edges may be negated.  Nodes include
  inputs, AND gates.
  - Some different variants, but we have 6 node types:
      - constant-false
      - primary input
      - register
      - AND gate
      - next-state
      - primary output.
  - Introduce our running example.
  - Useful for equivalence checking, model checking, synthesis

-----

Concrete defstobj form:

(defstobj aignet

   ;; Counters for different types of nodes
   (num-ins     :type (integer 0 *) :initially 0)
   (num-outs    :type (integer 0 *) :initially 0)
   (num-regs    :type (integer 0 *) :initially 0)
   (num-gates   :type (integer 0 *) :initially 0)
   (num-nxsts   :type (integer 0 *) :initially 0)

   ;; Counter for total number of nodes
   (num-nodes   :type (integer 0 *) :initially 1)

   ;; Node table: two 32-bit entries per node
   (nodes       :type (array (unsigned-byte 32) (2))
                :initially 0
                :resizable t)

   ;; Input/output/register arrays.
   ;; Supports a usage convention where transformations of the AIG may renumber node IDs
   ;; but not inputs/outputs, and not regs when preserving combinational equivalence.
   (ins        :type (array (unsigned-byte 32) (0))
               :initially 0
               :resizable t)
   (outs       :type (array (unsigned-byte 32) (0))
               :initially 0
               :resizable t)
   (regs       :type (array (unsigned-byte 32) (0))
               :initially 0
               :resizable t)

   ;; Inline accessor/updater functions for less fncall overhead
   :inline t)


Concrete representation of example circuit:

Node counters:
  2 PIs
  1 PO
  1 reg
  3 gates
  1 next-state
  9 nodes total

Nodetable contents:
Index              Data slots             Explanation
            (2 32-bit values per node)
            -----------------------
0                        | typ 0          Constant-false node
                         |
            -----------------------
1                        | typ 2          input i0
                PI num 0 | reg 0
            -----------------------
2                        | typ 2          input i1
                PI num 1 | reg 0
            -----------------------
3              nxst ID 5 | typ 2          register r0
               reg num 0 | reg 1
            -----------------------
4            fanin lit 5 | typ 1          gate g0 = ~i1 & r0
             fanin lit 6 |
            -----------------------
5            fanin lit 9 | typ 3          r0 next = ~g0
                reg ID 3 | reg 1
            -----------------------
6            fanin lit 1 | typ 1          gate g1 = 1 & i0
             fanin lit 2 |
            -----------------------
7            fanin lit 8 | typ 1          gate g2 = g0 & g1
            fanin lit 12 |
            -----------------------
8           fanin lit 14 | typ 3          output #0 = g2
                PO num 0 | reg 0
            -----------------------

PI table contents:    [ 1, 2 ]
Reg table contents:   [ 3 ]
PO table contents:    [ 8 ]


---------------------------------------

Abstract representation, complete:

((:po   14) ;; fanin
  (:gate 8   ;; fanin
         12) ;; fanin
  (:gate 1   ;; fanin
         2)  ;; fanin
  (:nxst 9   ;; fanin
         3)  ;; reg ID
  (:gate 5   ;; fanin
         6)  ;; fanin
  (:reg)
  (:pi)
  (:pi))

Notes on the abstract representation:

  - A node's ID is the length of its suffix

  - The constant-false node is implicit

  - PI/PO/register numbers are given by how many nodes of that type in
the node's suffix (excluding the node itself).

  - Certain invariants are implicit:
      - correspondence between PI/PO/reg numberings and tables
      - counts of node types and total numbers of nodes

  - Well-formedness isn't important
      - accessors "fix" any bad information pulled out of the structure
        so that they make sense


Abstract versus concrete accessor/updater definitions:

(num-nodes aignet)
  = [logic]          (+ 1 (node-count aignet))
  = [exec]           (nth *num-nodes* aignet)

(num-ins aignet)
  = [logic]          (stype-count :pi aignet)
  = [exec]           (nth *num-ins* aignet)

(id->type id aignet)
  = [logic]          (typecode (ctype (stype (car (lookup-id id aignet)))))
  = [exec]           (logand 3 (nth (* 2 id) (nth *nodesi* aignet)))
... but what you see in theorems is, e.g.,
       (equal (stype (car (lookup-id id aignet))) :gate) or
       (equal (ctype (stype (car (lookup-id id aignet)))) :input)

(innum->id n aignet)
  = [logic]         (node-count (lookup-stype n :pi aignet))
  = [exec]          (nth n (nth *insi* aignet))

(aignet-add-reg aignet)
  = [logic]         (cons '(:reg) aignet)
  = [exec]          (b* ((ro-num (num-regs aignet))
                         (nodes  (num-nodes aignet))
                         (aignet (add-reg aignet))
                         (aignet (add-node aignet))
                         (aignet (set-regnum->id ro-num nodes aignet))
                         ((mv slot0 slot1)
                          (mk-snode (in-type) 1 0 0 ro-num))
                         (aignet (update-node-slot nodes 0 slot0 aignet))
                         (aignet (update-node-slot nodes 1 slot1 aignet)))
                      aignet)

(aignet-add-gate fanin0 fanin1 aignet)
  = [logic]         (cons (gate-node (aignet-lit-fix fanin0 aignet)
                                     (aignet-lit-fix fanin1 aignet))
                          aignet)
  = [exec]          (b* ((nodes  (num-nodes aignet))
                         (aignet (add-node aignet))
                         (aignet (update-num-gates (+ 1 (lnfix (num-gates aignet))) aignet))
                         (phase (b-and (lit->phase f0 aignet)
                                       (lit->phase f1 aignet)))
                         ((mv slot0 slot1)
                          (mk-snode (gate-type) 0 phase (lit-val f0) (lit-val f1)))
                         (aignet (update-node-slot nodes 0 slot0 aignet))
                         (aignet (update-node-slot nodes 1 slot1 aignet)))
                      aignet)






Why abstract stobjs are nice:

  - Most "real" data structures contain redundant information in order
to improve computation time.  These redundancies are bad for reasoning
because each kind of redundancy requires an additional invariant.
     - E.g., PI table and counter is redundant with the node table.

  - If you can express the data structure logically as something
without these redundancies, then you don't need to keep track of these
invariants anymore.
     - With an abstract stobj, e.g., you've effectively proven these
       invariants ahead of time for all future functions you write.

  - May reduce the number of functions you need to reason about
     - Maybe just because of one's frame of mind when trying to
       figure out what's the simplest representation that will do what you want.
     - Aignet primitives are built (logically) on
            -  NODE-COUNT    (same as len)
            -  STYPE-COUNT   (count nodes with a certain tag, e.g., :pi)
            -  LOOKUP-ID     (find list suffix of a given size)
            -  LOOKUP-STYPE  (find list suffix with given number of nodes of the type)
            -  cons
            -  node constructors/accessors
         -- that's it.