Alists explaining what signals we want to extract from the simulation after each phase.
(stv-extraction-alists n lines alists-acc) → 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 . b) (bar . b) ... (bar[n] . b[n]))
The P2 alist binds something like:
((foo . a) ... (foo[n] . a[n]) (baz . d) ... (baz . 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.
(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)))))
(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)