Generating G-bindings from an STV in a particular way.
(stv-easy-bindings stv order) → *
- stv — The STV you are dealing with.
Guard (processed-stv-p stv).
- order — The variable order you want to use.
(stv-easy-bindings stv order) is a macro for proving theorems about
symbolic-test-vectors using gl. It returns a list of G-bindings
for use with def-gl-thm. That is, you can write something like:
(stv-easy-bindings (my-stv) '(opcode size special (:mix a b) c)))
This is probably only useful when:
- You are using GL in BDD mode, not some AIG or SAT based mode.
- You are running into performance problems when using the default
-autobinds from the defstv.
- You want to see if a different variable order performs better.
To use stv-easy-bindings, you just list (a subset of) the STV inputs in
priority order. For instance, in the above example, the opcode will get
the smallest indices, then size next, etc. You do not have to list
all of the STV variables. Any unmentioned variables will be assigned indices
after mentioned variables.
As in gl::auto-bindings, you can also use (:mix a b c ...) to
interleave the bits of a, b, c, ...; note that for this to work
these variables must all share the same width. This is generally useful for
data buses that are going to be combined together.
An especially nice feature of easy-bindings is that they automatically
adjust when inputs to the STV are resized, when new inputs are added, and when
irrelevant inputs are removed.
Definitions and Theorems
(defun stv-easy-bindings (stv order)
(declare (xargs :guard (processed-stv-p stv)))
(let ((__function__ 'stv-easy-bindings))
(declare (ignorable __function__))
(b* ((binds (stv-easy-bindings-main order stv))
(unbound (set-difference-equal (stv->ins stv)
(stv-easy-bindings-inside-mix unbound stv))))))