		Search-engine friendly clone of the ACL2 documentation.

Stv-process

Stv-fully-general-simulation-run

Run an n step, fully general simulation of a module.

Signature
(stv-fully-general-simulation-run n mod override-stbits) → (mv init-st in-alists nst-alists out-alists nil)
Arguments: n — How many phases to simulate.
Guard (posp n).; mod — The esim module.; override-stbits — List of override value and decision state bits.
Guard (symbol-listp override-stbits).
Returns: init-st — Initial state alist that we used. This is just generated by stv-fully-general-st-alist and is probably not very interesting.; in-alists — Input alists that we used at each phase. This is just generated by stv-fully-general-in-alists and is probably not very interesting.; nst-alists — A list of n alists that capture the fully general next-state after each phase.; out-alists — A list of n alists that capture the fully general outputs after each phase.; nil — An extra output which is always nil, for signature compatibility with stv-fully-general-simulation-debug.

This is a fully general simulation, so the nst/out-alists bind signal names to 4v-sexprs in terms of the variables in the init-st and in-alists.

See also stv-fully-general-simulation-debug, which produces the same outputs but also captures the internal signals after each phase.

We memoize this function so that if we're reusing an STV, we can just reuse the same general simulation repeatedly. BOZO maybe we should be memoizing the individual steps instead of the whole run, to get more cross-stv sharing.

Definitions and Theorems

Function: stv-fully-general-simulation-run

(defun
 stv-fully-general-simulation-run
 (n mod override-stbits)
 (declare (xargs :guard (and (posp n)
                             (symbol-listp override-stbits))))
 (let
    ((__function__ 'stv-fully-general-simulation-run))
    (declare (ignorable __function__))
    (b* ((in-alists (stv-fully-general-in-alists n mod))
         (init-st-alist (stv-fully-general-st-alist mod))
         (override-alists
              (stv-fully-general-in-alists-aux (- n 1)
                                               override-stbits nil))
         ((mv nsts outs)
          (ec-call (stv-run-esim mod in-alists
                                 override-alists init-st-alist))))
        (mv init-st-alist
            in-alists nsts outs nil))))