Convert the user-level input alist (which binds simulation variables to naturals) into a bit-level alist for 4v-sexpr-eval.
(stv-simvar-inputs-to-bits user-alist in-usersyms) → *
We try to translate every user-level binding, like
((opcode . *4vt*) (opcode . *4vt*) (opcode . *4vt*) (opcode . *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
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.
(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))))