		Search-engine friendly clone of the ACL2 documentation.

Stv-run

Stv-assemble-output-alist

Convert the bit-level bindings from after 4v-sexpr-eval into user-level bindings of the output simulation variables to naturals or X.

Signature
(stv-assemble-output-alist bit-out-alist out-usersyms) → *
Arguments: bit-out-alist — A fast alist that binds the output simulation variable bit names to their 4vp constants. This alist should have been produced by calling 4v-sexpr-eval on the relevant-signals sexprs of a processed-stv-p.; out-usersyms — An ordinary alist that binds each output 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-output-entry.

We recur down out-usersyms. For each output variable, we look up the values of its bits in bit-out-alist, and then try to combine these bits into a single integer value. If any bit is X, we just say the whole output is X.

Definitions and Theorems

Function: stv-assemble-output-alist

(defun stv-assemble-output-alist (bit-out-alist out-usersyms)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-assemble-output-alist))
  (declare (ignorable __function__))
  (b*
   (((when (atom out-usersyms)) nil)
    (rest
       (stv-assemble-output-alist bit-out-alist (cdr out-usersyms)))
    ((when (atom (car out-usersyms)))
     (raise "out-usersyms should be an alist.")
     rest)
    ((cons user-name bits)
     (car out-usersyms))
    (vals (vl2014::look-up-each-fast bits bit-out-alist))
    (true-val (4v-to-nat vals))
    (- (and (eq true-val 'x)
            (cw "Bits bound to X in ~x0: ~x1~%"
                user-name
                (collect-bits-bound-to-x bits bit-out-alist)))))
   (cons (cons user-name true-val) rest))))

Subtopics

Collect-bits-bound-to-x