Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Ipasir
Aignet
Base-api
Aignet-construction
Representation
Aignet-impl
Node
Network
Lookup-id
Lookup-stype
Aignet-extension-p
Aignet-nodes-ok
Aignet-outputs-aux
Aignet-nxsts-aux
Fanin
Aignet-outputs
Lookup-reg->nxst
Aignet-lit-fix
Aignet-fanins
Stype-count
Aignet-nxsts
Aignet-idp
Aignet-norm
Aignet-norm-p
Aignet-id-fix
Fanin-count
Proper-node-listp
Fanin-node-p
Node-list
Aignet-litp
Combinational-type
Typecode
Stypep
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
Math
Testing-utilities
Representation
Network
Reference guide for basic functions for working with the AIG network, i.e., a list of
node
s.
Subtopics
Lookup-id
Core function for looking up an AIG node in the logical AIG network by its ID.
Lookup-stype
Core function for looking up an input, output, or register in the logical AIG network by its IO number.
Aignet-extension-p
(aignet-extension-p new old)
determines if the aignet
new
is the result of building some new nodes onto another aignet
old
.
Aignet-nodes-ok
Basic well-formedness constraints for the AIG network.
Aignet-outputs-aux
Aignet-nxsts-aux
Fanin
(fanin which aignet)
gets the specified fanin from the first node of the input network and fixes it to be a valid fanin literal of the rest of the network.
Aignet-outputs
Lookup-reg->nxst
Look up the next-state node that corresponds to particular register node.
Aignet-lit-fix
(aignet-lit-fix x aignet)
fixes the
literal
x
to be a valid literal for this AIG network.
Aignet-fanins
Stype-count
(stype-count type x)
counts the number of
node
s whose
sequential-type
is
type
in the node list
x
.
Aignet-nxsts
Aignet-idp
Check whether a node ID is in bounds for this network.
Aignet-norm
Aignet-norm-p
Aignet-id-fix
Fix an ID so that it is valid for the aignet.
Fanin-count
Number of fanin nodes in the list of nodes
Proper-node-listp
(proper-node-listp x)
recognizes lists where every element satisfies
proper-node-p
.
Fanin-node-p
Node-list
A list of
node-p
objects.
Aignet-litp
Abbreviation for
(
aignet-idp
(
lit->var
x) aignet)
.