 An Abstract Stobj Representation of AndInverter 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 listbased model
e.g., a 5slot structure turns into a 5element list
an array slot of length N turns into a list of length N
Accessors/updaters: nth, updatenth
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/updatenth 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:
 constantfalse
 primary input
 register
 AND gate
 nextstate
 primary output.
 Introduce our running example.
 Useful for equivalence checking, model checking, synthesis

Concrete defstobj form:
(defstobj aignet
;; Counters for different types of nodes
(numins :type (integer 0 *) :initially 0)
(numouts :type (integer 0 *) :initially 0)
(numregs :type (integer 0 *) :initially 0)
(numgates :type (integer 0 *) :initially 0)
(numnxsts :type (integer 0 *) :initially 0)
;; Counter for total number of nodes
(numnodes :type (integer 0 *) :initially 1)
;; Node table: two 32bit entries per node
(nodes :type (array (unsignedbyte 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 (unsignedbyte 32) (0))
:initially 0
:resizable t)
(outs :type (array (unsignedbyte 32) (0))
:initially 0
:resizable t)
(regs :type (array (unsignedbyte 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 nextstate
9 nodes total
Nodetable contents:
Index Data slots Explanation
(2 32bit values per node)

0  typ 0 Constantfalse 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 constantfalse 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
 Wellformedness isn't important
 accessors "fix" any bad information pulled out of the structure
so that they make sense
Abstract versus concrete accessor/updater definitions:
(numnodes aignet)
= [logic] (+ 1 (nodecount aignet))
= [exec] (nth *numnodes* aignet)
(numins aignet)
= [logic] (stypecount :pi aignet)
= [exec] (nth *numins* aignet)
(id>type id aignet)
= [logic] (typecode (ctype (stype (car (lookupid id aignet)))))
= [exec] (logand 3 (nth (* 2 id) (nth *nodesi* aignet)))
... but what you see in theorems is, e.g.,
(equal (stype (car (lookupid id aignet))) :gate) or
(equal (ctype (stype (car (lookupid id aignet)))) :input)
(innum>id n aignet)
= [logic] (nodecount (lookupstype n :pi aignet))
= [exec] (nth n (nth *insi* aignet))
(aignetaddreg aignet)
= [logic] (cons '(:reg) aignet)
= [exec] (b* ((ronum (numregs aignet))
(nodes (numnodes aignet))
(aignet (addreg aignet))
(aignet (addnode aignet))
(aignet (setregnum>id ronum nodes aignet))
((mv slot0 slot1)
(mksnode (intype) 1 0 0 ronum))
(aignet (updatenodeslot nodes 0 slot0 aignet))
(aignet (updatenodeslot nodes 1 slot1 aignet)))
aignet)
(aignetaddgate fanin0 fanin1 aignet)
= [logic] (cons (gatenode (aignetlitfix fanin0 aignet)
(aignetlitfix fanin1 aignet))
aignet)
= [exec] (b* ((nodes (numnodes aignet))
(aignet (addnode aignet))
(aignet (updatenumgates (+ 1 (lnfix (numgates aignet))) aignet))
(phase (band (lit>phase f0 aignet)
(lit>phase f1 aignet)))
((mv slot0 slot1)
(mksnode (gatetype) 0 phase (litval f0) (litval f1)))
(aignet (updatenodeslot nodes 0 slot0 aignet))
(aignet (updatenodeslot 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
 NODECOUNT (same as len)
 STYPECOUNT (count nodes with a certain tag, e.g., :pi)
 LOOKUPID (find list suffix of a given size)
 LOOKUPSTYPE (find list suffix with given number of nodes of the type)
 cons
 node constructors/accessors
 that's it.