Stv-run-esim
- Signature
(stv-run-esim mod in-alists state-alists initial-state)
→
(mv nsts outs)
- Arguments
- mod — The module to run.
Guard (good-esim-modulep mod).
- in-alists — A list of N alists, to be used at each phase.
- state-alists — A list of N alists, to override particular state bits.
- initial-state — Initial state to use.
- Returns
- nsts — A list of next-state alists.
- outs — A list of outputs alists.
Definitions and Theorems
Function: stv-run-esim
(defun stv-run-esim (mod in-alists state-alists initial-state)
(declare (xargs :guard (good-esim-modulep mod)))
(declare (xargs :guard (eql (len in-alists)
(len state-alists))))
(let ((__function__ 'stv-run-esim))
(declare (ignorable __function__))
(b* (((when (atom in-alists)) (mv nil nil))
(state-alist (append-without-guard (car state-alists)
initial-state))
((mv nst1 out1)
(esim-sexpr-simp mod (car in-alists)
state-alist))
((mv nst-rest out-rest)
(stv-run-esim mod (cdr in-alists)
(cdr state-alists)
nst1)))
(mv (cons nst1 nst-rest)
(cons out1 out-rest)))))
