6. Writing :g-bindings forms
In a typical def-gl-thm command, the :g-bindings should have an
entry for every free variable in the theorem. Here is an example that shows
some typical bindings.
:g-bindings '((flag (:g-boolean . 0))
(a-bus (:g-integer 1 3 5 7 9))
(b-bus (:g-integer 2 4 6 8 10))
(mode (:g-ite (:g-boolean . 11) exact . fast))
(opcode #b0010100))
These bindings allow flag to take an arbitrary Boolean value,
a-bus and b-bus any five-bit signed integer values, mode either
the symbol exact or fast, and opcode only the value 20.
(Aside: Note that since #b0010100 is not within a :g-boolean or
:g-integer form, it is not the index of a Boolean variable.
Instead, like the symbols exact and fast, it is just an ordinary ACL2
constant that stands for itself, i.e., 20.)
These :g-boolean and :g-integer are called shape-specs.
They are similar to the symbolic objects GL uses to compute with, except that
natural number indices take the places of Boolean expressions. The indices
used throughout all of the bindings must be distinct, and represent free,
independent Boolean variables.
In BDD mode, these indices have additional meaning: they specify the BDD
variable ordering, with smaller indices coming first in the order. This
ordering can greatly affect performance. In AIG mode the choice of indices has
no particular bearing on efficiency.
How do you choose a good BDD ordering? It is often good to interleave the
bits of data buses that are going to be combined in some way. It is also
typically a good idea to put any important control signals such as opcodes and
mode settings before the data buses.
Often the same :g-bindings can be used throughout several theorems,
either verbatim or with only small changes. In practice, we almost always
generate the :g-bindings forms by calling functions or macros. One
convenient function is
(g-int start by n)
which generates a :g-integer form with n bits, using
indices that start at start and increment by by. This is
particularly useful for interleaving the bits of numbers, as we did for the
a-bus and b-bus bindings above:
(g-int 1 2 5) ---> (:g-integer 1 3 5 7 9)
(g-int 2 2 5) ---> (:g-integer 2 4 6 8 10)
Writing out :g-bindings and getting all the indices can be tedious.
See auto-bindings for a convenient macro that helps ensure that all the
indices are different.
