		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-extraction-alists

Alists explaining what signals we want to extract from the simulation after each phase.

Signature
(stv-extraction-alists n lines alists-acc) → alists-acc
Arguments: n — Initially this is the total number of phases. It will counts down from the max phase to 0.
Guard (natp n).; lines — Constant. Expanded output or internals lines.
Guard (true-list-listp lines).; alists-acc — Accumulator, initially nil.
Returns: alists-acc — A list of alists that say, after each step, which output bits we want to collect, and how to name them.
Type (true-listp alists-acc), given (true-listp alists-acc).

The basic idea is that if we have a list of outputs lines like:

(foo  _ _ a _)
(bar  _ b _ c)
(baz  _ _ d _)

Then we will want to create four alists, one for each phase. The P0 alist is empty. The P1 alist binds something like

((bar[0] . b[0])
 (bar[1] . b[1])
 ...
 (bar[n] . b[n]))

The P2 alist binds something like:

((foo[0] . a[0])
  ...
 (foo[n] . a[n])
 (baz[0] . d[0])
  ...
 (baz[0] . d[k]))

And so on. That is, each of these extraction alists says, for a particular phase, the names of the output signals we want to extract from the simulation, and which bit of which simulation variable the name corresponds to.

Definitions and Theorems

Function: stv-extraction-alists

(defun stv-extraction-alists (n lines alists-acc)
  (declare (xargs :guard (and (natp n) (true-list-listp lines))))
  (let ((__function__ 'stv-extraction-alists))
    (declare (ignorable __function__))
    (let* ((nth-alist (stv-nth-extraction-alist n lines nil))
           (alists-acc (cons nth-alist alists-acc)))
      (if (zp n)
          alists-acc
        (stv-extraction-alists (- n 1)
                               lines alists-acc)))))

Theorem: true-listp-of-stv-extraction-alists

(defthm true-listp-of-stv-extraction-alists
  (implies
       (true-listp alists-acc)
       (b* ((alists-acc (stv-extraction-alists n lines alists-acc)))
         (true-listp alists-acc)))
  :rule-classes :rewrite)

Subtopics

Stv-nth-extraction-alist: Add the bindings for name to entryN to the NTH-ALIST-ACC