Aig-and
(aig-and x1 x2 ...) constructs an AIG representing (and x1 x2
...).
The main function is aig-binary-and. It implements
something like the algorithm described in:
In particular, see Table 2 in that paper, which describes optimization rules
that are ``locally size decreasing without affecting global sharing
negatively.''
We try to implement these rules in aig-and-main, which returns:
(mv status arg1 arg2)
The status is either:
- :fail if no rule applies, in which case arg1 and arg2 are
just copies of x and y and we need to construct a new AND node that
joins them together;
- :subterm if a rewrite rule applies that reduces the AND of x and
y to either a constant or to a subterm of x or y. This subterm
is returned as both arg1 and arg2. In this case, we assume there is
no more rewriting to be done and just return the reduced subterm.
- :reduced if a rewrite rule applies that reduces the AND in some
interesting way, where it is no longer a proper subterm of x or y.
In this case, it may be possible to further reduce arg1 and arg2,
so we want to recursively rewrite them.
aig-and itself is a macro which extends aig-binary-and across many
arguments. As one last special optimization, when there is more than one
argument we try to "short-circuit" the computation and avoid evaluating some
arguments.
See also aig-and-dumb, which is much less sophisticated but may be
easier to reason about in certain cases where you really care about the
structure of the resulting AIGs.
A June 2015 experiment suggests that, for a particular 80-bit floating point
addition problem, this fancier algorithm improves the size of AIGs produced by
sv by about 3% when measured either by unique AND nodes or by unique
conses.
Macro: aig-and
(defmacro aig-and (&rest args)
(cons 'mbe
(cons ':logic
(cons (aig-and-macro-logic-part args)
(cons ':exec
(cons (aig-and-macro-exec-part args)
'nil))))))
Subtopics
- Aig-and-main
- And-Node, Main Optimizations, Non-Recursive.
- Aig-and-pass6a
- Level 3 Substitution Rules, Single Direction.
- Aig-and-pass5
- Level 2, Resolution Rule.
- Aig-and-pass3
- Level 2 Contradiction Rule 2 and all Level 4 Rules.
- Aig-and-pass4a
- Level 2, Subsumption Rules 1 and 2, Single Direction.
- Aig-and-pass6
- Level 3 Substitution Rules, Both Directions.
- Aig-and-pass2a
- Level 2 Contradiction Rule 1 and Idempotence Rule, Single Direction.
- Aig-and-pass2
- Level 2 Contradiction Rule 1 and Idempotence Rule, Both Directions.
- Aig-and-pass4
- Level 2, Subsumption Rules 1 and 2, Both Directions.
- Aig-and-dumb
- (aig-and-dumb x y) is a simpler alternative to aig-and.
- Aig-negation-p
- (aig-negation-p x y) determines if the AIGs x and y
are (syntactically) negations of one another.
- Aig-and-pass1
- Level 1 simplifications.
- Aig-binary-and
- (aig-binary-and x y) constructs an AIG representing (and x y).
- Aig-and-macro-exec-part
- Generates the :exec part for a aig-and MBE call.
- Aig-and-macro-logic-part
- Generates the :logic part for a aig-and MBE call.
