		Search-engine friendly clone of the ACL2 documentation.

Stv-run

Stv-simvar-inputs-to-bits

Convert the user-level input alist (which binds simulation variables to naturals) into a bit-level alist for 4v-sexpr-eval.

Signature
(stv-simvar-inputs-to-bits user-alist in-usersyms) → *
Arguments: user-alist — The alist provided by the user that gives values to the input simulation variables. Each value should be a natural number that is in the range for that simulation variable.; in-usersyms — A fast alist that binds each input simulation variable for the STV with a list of variables that represent its bits; see stv-compile, but in particular see the usersyms output of stv-expand-input-entry.

We try to translate every user-level binding, like (opcode . 7), into a set of bit-level bindings, say something like:

((opcode[0] . *4vt*)
 (opcode[1] . *4vt*)
 (opcode[2] . *4vt*)
 (opcode[3] . *4vf*)
 ...)

For each input simulation variable bound in the user-level alist, we basically just need to look up the names of its bits in the in-usersyms alist, explode the value into 4vp bits, and then pairing up the bit names with the values. In the process, we do some basic sanity checking to make sure that the names being bound exist and that the provided values are in range.

The net result is a new alist that is suitable for 4v-sexpr-eval that we can use to evaluate output expressions.

We don't check for duplicates in the user-alist, and if there are duplicates it could lead to duplicate bindings in our resulting bit-level alist. However, the alist semantics are preserved because shadowed bindings are still shadowed in the bit-level alist.

Definitions and Theorems

Function: stv-simvar-inputs-to-bits

(defun stv-simvar-inputs-to-bits (user-alist in-usersyms)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-simvar-inputs-to-bits))
  (declare (ignorable __function__))
  (b*
   (((when (atom user-alist)) nil)
    (rest (stv-simvar-inputs-to-bits (cdr user-alist)
                                     in-usersyms))
    ((when (atom (car user-alist)))
     (cw
      "stv-simvar-inputs-to-bits: skipping malformed alist entry ~x0.~%"
      (car user-alist))
     rest)
    (name (caar user-alist))
    (val (cdar user-alist))
    (look (hons-get name in-usersyms))
    ((unless look)
     (raise
       "Value given for ~x0, but this is not a simulation variable."
       name)
     rest)
    (vars (cdr look))
    (nvars (len vars))
    (vals
     (cond
      ((eq val *4vx*) (replicate nvars *4vx*))
      ((and (natp val) (< val (ash 1 nvars)))
       (bool-to-4v-lst (int-to-v val nvars)))
      (t
       (progn$
        (raise
         "Value ~x0 given for ~x1, but this value is not X ~
                             or in range for a ~x2-bit unsigned number."
         val name nvars)
        (replicate nvars *4vx*))))))
   (safe-pairlis-onto-acc vars vals rest))))