		Search-engine friendly clone of the ACL2 documentation.

Stv-debug

Stv-fully-general-simulation-debug

Run an n step, fully general simulation of mod just like stv-fully-general-simulation-run, but also gather the fully general expressions for internal signals.

Signature
(stv-fully-general-simulation-debug n mod override-stbits) → (mv init-st in-alists nst-alists out-alists int-alists)
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 — As in stv-fully-general-simulation-run.; in-alists — As in stv-fully-general-simulation-run.; nst-alists — As in stv-fully-general-simulation-run.; out-alists — As in stv-fully-general-simulation-run.; int-alists — A list of n alists that capture the fully general internal signals after each phase.

This is practically identical to stv-fully-general-simulation-run, except that it also gathers up and returns a list of int-alists which contain the expressions for the internal signals of the module.

These expressions are useful for generating waveforms for debugging simulations. We could have just had stv-fully-general-simulation-run always compute them, but computing the internal signals can be expensive so we want to avoid it unless we're actually doing debugging.

Due to the structure of esim, we get a lot of memoized sharing between the -run and -debug functions. This works out very nicely, so that it's not much more expensive to do a -debug after first doing a -run than it is to just do a -debug from the beginning.

We memoize this function so that if we're reusing an STV, we can just reuse the same general simulation repeatedly as we debug with different values. BOZO as with the -run function, maybe we should be doing the memoization at the level of individual steps, instead of memoizing the whole thing.

Definitions and Theorems

Function: stv-fully-general-simulation-debug

(defun stv-fully-general-simulation-debug (n mod override-stbits)
 (declare (xargs :guard (and (posp n)
                             (symbol-listp override-stbits))))
 (let ((__function__ 'stv-fully-general-simulation-debug))
   (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 internals)
      (ec-call (stv-run-esim-debug mod in-alists
                                   override-alists init-st-alist))))
    (mv init-st-alist
        in-alists nsts outs internals))))

Theorem: len-of-stv-fully-general-simulation-debug-1

(defthm len-of-stv-fully-general-simulation-debug-1
  (equal (len (mv-nth 1
                      (stv-fully-general-simulation-debug
                           nphases mod override-stbits)))
         (nfix nphases)))

Theorem: len-of-stv-fully-general-simulation-debug-2

(defthm len-of-stv-fully-general-simulation-debug-2
  (equal (len (mv-nth 2
                      (stv-fully-general-simulation-debug
                           nphases mod override-stbits)))
         (nfix nphases)))

Theorem: len-of-stv-fully-general-simulation-debug-3

(defthm len-of-stv-fully-general-simulation-debug-3
  (equal (len (mv-nth 3
                      (stv-fully-general-simulation-debug
                           nphases mod override-stbits)))
         (nfix nphases)))

Theorem: len-of-stv-fully-general-simulation-debug-4

(defthm len-of-stv-fully-general-simulation-debug-4
  (equal (len (mv-nth 4
                      (stv-fully-general-simulation-debug
                           nphases mod override-stbits)))
         (nfix nphases)))

Theorem: cons-list-listp-of-stv-fully-general-simulation-debug-1

(defthm cons-list-listp-of-stv-fully-general-simulation-debug-1
  (cons-list-listp (mv-nth 1
                           (stv-fully-general-simulation-debug
                                nphases mod override-stbits))))