		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-compile

Syntactically transform a symbolic test vector, readying it for evaluation, debugging, etc.

Signature
(stv-compile stv mod) → cstv
Arguments: stv — An stvdata-p that has already had its lines widened and any Verilog-style names expanded; see stv-widen and stv-expand.
Guard (stvdata-p stv).; mod — The esim module this STV is about.
Guard (good-esim-modulep mod).
Returns: cstv — Type (equal (compiled-stv-p cstv) (if cstv t nil)).

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 |foo[0]| to |foo[0].P3| during phase 3, and so forth. The idea is that instead of re-running esim for each STV, we will just specialize this alist by using 4v-sexpr-restrict to replace |foo[0].P3| with whatever value we want for |foo[0]| at phase 3.

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.

Definitions and Theorems

Function: stv-compile

(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)))

Theorem: return-type-of-stv-compile

(defthm return-type-of-stv-compile
  (b* ((cstv (stv-compile stv mod)))
    (equal (compiled-stv-p cstv)
           (if cstv t nil)))
  :rule-classes :rewrite)

Subtopics

Stv-expand-input-entry: Convert a single user-level input value (e.g., 17, X, abus, etc) into a list of 4v-sexprs.
Stv-expand-output-entry: Convert a single user-level output/internal value (e.g., _, result) into a list of 4v-sexprs.
Stv-restrict-alist: Construct an alist binding fully-general input names (for all phases) to 4v-sexprs derived from the symbolic test vector.
Stv-extraction-alists: Alists explaining what signals we want to extract from the simulation after each phase.
Stv-expand-input-lines: Extend stv-expand-input-entry across a list of lines.
Stv-expand-input-entries: Extend stv-expand-input-entry across a line.
Stv-expand-output-entries: Extend stv-expand-output-entry across a line.
Stv-expand-output-lines: Extend stv-expand-output-entry across a list of lines.
Stv-expand-internal-lines: Extend stv-expand-internal-line across a list of lines.
Stv-expand-internal-line
Stv-forge-state-bit: Generate the name for a state bit, like foo!bar!baz!inst!S, given a list of instance names and the name of the state bit.
Stv-gensyms: Generate a list of symbols, (foo[0] ... foo[n-1]).
Safe-pairlis-onto-acc: Just pairlis$ onto an accumulator, but for safety cause an error if the lists to pair up aren't the same length.