Parametrize
Transform the AIG so that some conditions assumed to be untrue don't
affect the logical equivalence of nodes, using BDDs to compute a
hopefully-efficient parametrization.
This is intended to have a similar effect as the observability-fix transform, but perhaps making fraiging more efficient by
making the substitution applied to the primary inputs more transparent to
random simulation vectors. Currently it only works in the context of
m-assumption, n-output transforms, i.e. it preserves full combinational
equivalence for the first m outputs, then combinational equivalence under the
assumption that the first m outputs are true for the next n outputs.
Usage
In the context of a sequence of m-assumption-n-output AIG
transforms, this transform is invoked by including a parametrize-config
object in the list of transforms.
Concept
Like the observability transform, this replaces the PIs involved in the
assumed condition with new expressions. These expressions equal the PIs
themselves when the condition holds, and they evaluate to some values for which
the condition does hold otherwise. That is, if the inputs are ins[i] for
i=0 to n-1, the parametrized inputs for a satisfiable condition C(ins) satisfies
C(Param(C,ins)) and C(ins) => Param(C,ins) = ins. The
parametrization by C can be thought of as a fixing function: it maps the
set of all input vectors into the subset that satisfy C, keeping those that already
satisfy C fixed.
So far, this holds for both the parametrize and
observability transforms. The difference is in how inputs that do not satisfy
C are mapped to ones that do.
The observability transform maps all inputs that don't satisfy C to a
fixed value that does satisfy it, except that inputs C doesn't depend on
keep their values. This is simple, but has one big downside: it can make
random simulation nearly useless, because if most input vectors do not satisfy
C and C depends on most input variables, then most randomly-generated
vectors will uselessly map to the same value of those inputs. It also means
that the substituted value for every variable involved in the condition depends
on the whole condition, regardless of what the particular constraints on that
variable are -- this makes strategies for FRAIGing such as level limiting and
dependency limiting much less useful.
The parametrize transform uses a different scheme that can potentially
distribute randomly-generated input vectors much more evenly over the set of
inputs that satisfy C. It works by using BDD parametrization. We fix an
ordering of the input variables (the BDD ordering) and translate the assumption
C into a BDD. Traversing this BDD lets us generate a set of BDDs giving
parametrized values for each of the inputs. The parametrized input vector
resulting from a particular input vector can be found by traversing the input
vector according to the BDD variable order. We maintain a cube of variable
assignments starting with the empty (constant-true) cube, for which C &
cube should always be satisfiable (using the assumption that C is
satisfiable). For each variable k in the BDD order, let v be the
value of k in the input vector. We check whether C & cube & (k=v) is
still satisfiable. If so, then we add k=v to the cube; if not, we add
k=~v to the cube; either way, C & cube remains satisfiable, and we
continue on with the next variable in the order. Once all variables have had
assignments added to the cube, the cube then gives the parametrized assignment
satisfying C, and if the original input vector satisfied C, then the
resulting one is the same since C & cube & (k=v) was satisfiable
throughout the algorithm.
Subtopics
- Aignet-parametrize-output-ranges
- Aignet-parametrize-copy-set-regs
- Aignet-parametrize-copy-set-ins
- Aignet-parametrize-collect-bdd-order-aux
- Aignet-parametrize-collect-bdd-order
- Aignet-output-range-conjoin-ubdds
- Aignet-output-range-collect-in/reg-ubdd-order
- Aignet-finish-reg-ubdd-order
- Aignet-finish-in-ubdd-order
- Aignet-copy-dfs-output-range
- Aignet-parametrize-m-n
- Aignet-node-to-ubdd
- Aignet-output-range-to-ubdds
- Ubdd-to-aignet
- Aignet-parametrize-copy-init
- Parametrize-config
- Config object for the parametrize AIG transform
- Parametrize-output-type
- Indicator of how the parametrize transform should treat a range of outputs
- Ubdd-arr-to-param-space
- Copy-lits-compose
- Bitarr-range-1bit-indices
- Bitarr-range-count
- Aignet-count-ubdd-branches-wrap
- Ubdd-to-aignet-memo-ok
- Aignet-node-to-ubdd-build-cond
- Copy-lits-compose-in-place
- Bitarr-range-set
- Ubdd/level
- Ubdd-arr
- Abstract stobj: logically this just represents a list of
|ACL2|::|UBDDP|s, but it is
implemented as an array.
- Ubdd-arr-max-depth
- Aignet-count-ubdd-branches
- Ubdd-negate-cond
- Ubdd-apply-gate
- Aignet-node-to-ubdd-short-circuit-cond
- Bits->bools
- Eval-ubddarr
- Ubdd-to-aignet-memo
- An alist mapping ubdd/level-p to litp.
- Parametrize-output-type-map
- An alist mapping symbolp to parametrize-output-type-p.
- Lubdd-fix
