Syntactically transform a symbolic test vector, readying it for evaluation, debugging, etc.
(stv-compile stv mod) → cstv
Compiling an STV involves doing lots of error checking to ensure the STV is syntactically well-formed, only refers to legitimate inputs and outputs, and so forth. After sanity checking, our basic goal is to compile the STV into a form that functions like stv-run and stv-debug can efficiently process.
In particular, after (successfully) compiling an STV we obtain a compiled-stv-p structure that says says how many steps we need to run for, explains the mappings from user-level simulation variables to their internal bit-encodings, and and has pre-computed alists for restricting the a esim run and extracting the results.
Compilation is a syntactic process that is relatively cheap. We memoize it mainly in the hopes of keeping the various alists we create the same across multiple evaluations of an STV.
Note that to reuse the same esim simulations across related STVs, our
basic approach in stv-run is to do a fully general simulation of the
module for N cycles. In this general simulation, we set
The function stv-restrict-alist pre-computes these bindings. Essentially it just needs to build a big alist that binds the suffixed input names to the sexprs that we generated in stv-expand-input-lines, above.
The outputs are somewhat similar. The function stv-extraction-alists builds a list of alists that say, for each step, which output bits we want to collect and how we want to name them.
(defun stv-compile (stv mod) (declare (xargs :guard (and (stvdata-p stv) (good-esim-modulep mod)))) (let ((__function__ 'stv-compile)) (declare (ignorable __function__)) (b* (((stvdata stv) stv) (nphases (stv-number-of-phases stv)) ((unless (posp nphases)) (raise "Trying to compile an STV without any phases?")) (override-paths (stv-append-alist-keys stv.overrides)) (mod (stv-cut-module override-paths mod)) (in-usersyms nil) ((mv inputs gensyms in-usersyms) (stv-expand-input-lines stv.inputs nil in-usersyms)) (restrict-alist nil) (restrict-alist (stv-restrict-alist inputs restrict-alist)) (out-usersyms nil) ((mv outputs out-usersyms) (stv-expand-output-lines stv.outputs out-usersyms)) ((mv internals out-usersyms) (stv-expand-internal-lines stv.internals out-usersyms mod)) (out-extract-alists (stv-extraction-alists (- nphases 1) outputs nil)) (int-extract-alists (stv-extraction-alists (- nphases 1) internals nil)) ((mv override-ins override-outs in-usersyms out-usersyms) (stv-expand-override-lines stv.overrides in-usersyms out-usersyms)) (restrict-alist (stv-restrict-alist override-ins restrict-alist)) (nst-extract-alists (stv-extraction-alists (- nphases 1) override-outs nil)) (all-in-bits (alist-keys restrict-alist)) ((unless (uniquep all-in-bits)) (raise "Name clash. Multiple input/initial bindings were generated ~ for ~x0." (duplicated-members all-in-bits))) (in-simvars (alist-keys in-usersyms)) (out-simvars (alist-keys out-usersyms)) ((unless (and (uniquep in-simvars) (uniquep out-simvars) (symbol-listp in-simvars) (symbol-listp out-simvars))) (raise "Programming error. in-simvars or out-simvars aren't unique ~ symbols. This shouldn't be possible.")) (all-in-bits (append-alist-vals-exec in-usersyms gensyms)) ((unless (uniquep all-in-bits)) (raise "Name clash for ~x0." (duplicated-members all-in-bits))) (override-bits (stv-append-alist-keys override-ins)) ((unless (symbol-listp override-bits)) (raise "Programming error -- override-bits should be a symbol-list: ~x0" override-bits)) (ret (make-compiled-stv :nphases nphases :restrict-alist restrict-alist :out-extract-alists out-extract-alists :int-extract-alists int-extract-alists :nst-extract-alists nst-extract-alists :override-bits override-bits :in-usersyms (make-fast-alist (rev in-usersyms)) :out-usersyms (make-fast-alist (rev out-usersyms)) :expanded-ins inputs :override-paths override-paths))) (fast-alist-free in-usersyms) (fast-alist-free out-usersyms) ret)))
(defthm return-type-of-stv-compile (b* ((cstv (stv-compile stv mod))) (equal (compiled-stv-p cstv) (if cstv t nil))) :rule-classes :rewrite)